diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp
index 8d612cef860..0f4bef68fda 100644
--- a/src/solvers/prop/bdd_expr.cpp
+++ b/src/solvers/prop/bdd_expr.cpp
@@ -58,15 +58,6 @@ mini_bddt bdd_exprt::from_expr_rec(const exprt &expr)
 
     return op0==op1;
   }
-  else if(expr.id()==ID_iff)
-  {
-    assert(expr.operands().size()==2);
-
-    mini_bddt op0=from_expr_rec(expr.op0());
-    mini_bddt op1=from_expr_rec(expr.op1());
-
-    return op0==op1;
-  }
   else if(expr.id()==ID_if)
   {
     const if_exprt &if_expr=to_if_expr(expr);
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index 40d895492be..284dd2f8272 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -78,8 +78,6 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
     operator_str = u8"\u2260"; // /=, U+2260
   else if(src.id() == ID_implies)
     operator_str = u8"\u21d2"; // =>, U+21D2
-  else if(src.id() == ID_iff)
-    operator_str = u8"\u21d4"; // <=>, U+21D4
   else
     operator_str = id2string(src.id());
 
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 287eef5dc89..067c91e1c17 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -41,7 +41,6 @@ IREP_ID_ONE(member_name)
 IREP_ID_TWO(C_member_name, #member_name)
 IREP_ID_TWO(equal, =)
 IREP_ID_TWO(implies, =>)
-IREP_ID_TWO(iff, "<=>")
 IREP_ID_ONE(and)
 IREP_ID_ONE(nand)
 IREP_ID_ONE(or)
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 1b1591e81b1..96e94afab13 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -2307,7 +2307,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result=simplify_unary_plus(expr) && result;
   else if(expr.id()==ID_not)
     result=simplify_not(expr) && result;
-  else if(expr.id()==ID_implies || expr.id()==ID_iff ||
+  else if(expr.id()==ID_implies ||
           expr.id()==ID_or      || expr.id()==ID_xor ||
           expr.id()==ID_and)
     result=simplify_boolean(expr) && result;
diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp
index 99a548927e1..06bd5f505a8 100644
--- a/src/util/simplify_expr_boolean.cpp
+++ b/src/util/simplify_expr_boolean.cpp
@@ -40,38 +40,6 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
     simplify_node(expr);
     return false;
   }
-  else if(expr.id()==ID_iff)
-  {
-    if(operands.size()!=2 ||
-       operands.front().type().id()!=ID_bool ||
-       operands.back().type().id()!=ID_bool)
-      return true;
-
-    if(operands.front().is_false())
-    {
-      expr.id(ID_not);
-      operands.erase(operands.begin());
-      return false;
-    }
-    else if(operands.front().is_true())
-    {
-      exprt tmp(operands.back());
-      expr.swap(tmp);
-      return false;
-    }
-    else if(operands.back().is_false())
-    {
-      expr.id(ID_not);
-      operands.erase(++operands.begin());
-      return false;
-    }
-    else if(operands.back().is_true())
-    {
-      exprt tmp(operands.front());
-      expr.swap(tmp);
-      return false;
-    }
-  }
   else if(expr.id()==ID_xor)
   {
     bool result=true;