Biconditional elimination: the A ↔ B rewrite and the ↔E rule
Biconditional elimination rewrites A <-> B as (A AND B) OR (NOT A AND NOT B): both true, or both false. In natural deduction the same name means the inference rule ↔E: from A <-> B and A, infer B, and from A <-> B and B, infer A.
A biconditional is rewritten as “both true” OR “both false”.
“A if and only if B” holds exactly when A and B have the same value. Spelling that out gives the two cases of the right-hand side. The law is the bridge between the logician's biconditional and the engineer's XNOR gate: the engine proves XNOR(A, B) = A <-> B as a separate law, so the three forms are interchangeable.
The normal-form converter applies this elimination to reach a CNF or DNF. The simplifier keeps the biconditional as one operator and folds only the cases with a constant, equal or complementary operands, so A <-> A becomes TRUE in one step. Its negation, by De Morgan, is (A OR B) AND (NOT A OR NOT B), which is exactly XOR in product-of-sums form; the comparison of implication and biconditional shows both on one table.
The four-row proof is below.
Statement
A <-> B = (A AND B) OR (NOT A AND NOT B) Proof by truth table: A <-> B = (A AND B) OR (NOT A AND NOT B)
| # | A | B | lhs | rhs |
|---|---|---|---|---|
| 0 | FALSE | FALSE | TRUE | TRUE |
| 1 | FALSE | TRUE | FALSE | FALSE |
| 2 | TRUE | FALSE | FALSE | FALSE |
| 3 | TRUE | TRUE | TRUE | TRUE |
The same law in four notations
A <-> BA <-> BA ↔ BA ↔ BA \leftrightarrow B(A AND B) OR (NOT A AND NOT B)(A && B) || (!A && !B)(A ∧ B) ∨ (¬A ∧ ¬B)(A·B) + (A'·B')\left(A \cdot B\right) + \left(\overline{A} \cdot \overline{B}\right)Biconditional elimination in natural deduction (↔E)
In a natural-deduction proof, biconditional elimination (↔E) is a rule of inference: from a line A <-> B and a line A, you may write B; from A <-> B and B, you may write A. It is modus ponens in either direction, because A <-> B holds exactly when A -> B and B -> A both hold.
Both argument forms are valid: no row makes A <-> B and one side TRUE while the other side is FALSE, which the rewrite on this page makes plain, since A <-> B is TRUE only when the two sides are equal. The argument validity checker confirms either form when you enter the premises and the conclusion. Tangibool checks arguments by truth table; it does not build natural-deduction proofs line by line.
The common slip
Chaining biconditionals without brackets. A <-> B <-> C is rejected by the parser on purpose: both groupings have the same table, but the chain is easily misread as “all three are equal”, which it does not mean, since it is FALSE when all three are FALSE; write (A <-> B) <-> C or A <-> (B <-> C).
Questions
How is “A exactly when B” different from “A if B”?
“A if B” is the one-way implication B -> A; “exactly when” adds the other direction and is the biconditional. The equivalence checker shows that A <-> B and B -> A differ on the row A = TRUE, B = FALSE.
What is the biconditional elimination rule?
In natural deduction, ↔E: from A <-> B and one side, infer the other side. In Boolean algebra the same name means the rewrite this page proves, A <-> B as (A AND B) OR (NOT A AND NOT B).
Related
Lesson that teaches this
Tools
- Boolean algebra calculator and simplifier with steps (every law named and verified)
- Logical equivalence checker: two expressions, exact verdict, counterexample
Practice
See also
- Argument validity checker: premises, conclusion, counterexample or proof
- Biconditional (↔, if and only if): truth table and examples
- XNOR elimination: XNOR(A, B) = A ↔ B
- XOR elimination: A XOR B = (A AND NOT B) OR (NOT A AND B)
- Implication vs biconditional
Laws
Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build . Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.