Skip to content
EN ES
Sign in Open the app

XNOR elimination: XNOR(A, B) = A ↔ B

XNOR elimination rewrites XNOR(A, B) as the biconditional A <-> B: the gate that is true when both inputs are equal is the connective that says “if and only if”.

Engine name: XNOR eliminationFR: Élimination du XNORDE: Auflösung von XNOR

XNOR is rewritten as a biconditional.

XNOR is the negation of XOR, so it is true when the inputs agree: both true or both false. That is exactly the biconditional, which is why the engine proves the identity as a law and accepts either spelling. From there, biconditional elimination gives (A AND B) OR (NOT A AND NOT B).

The equality comparator in the worked examples is built from XNOR gates for this reason: two bits are equal when their XNOR is true, and two two-bit numbers are equal when both XNORs are.

The four-row proof is below. The operator page on XNOR shows the gate table and the same function written as a biconditional.

Statement

XNOR(A, B) = A <-> B

Proof by truth table: XNOR(A, B) = A <-> B

XNOR(A, B) = A <-> B
#ABlhsrhs
0FALSEFALSETRUETRUE
1FALSETRUEFALSEFALSE
2TRUEFALSEFALSEFALSE
3TRUETRUETRUETRUE
lhs ≡ rhs holds · lhs and rhs agree on every assignment. · Exhaustively checked and solver cross-checked · 4 rows

The same law in four notations

WordsXNOR(A, B)
ProgrammingXNOR(A, B)
MathematicalXNOR(A, B)
AlgebraXNOR(A, B)
LaTeX\overline{A \oplus B}
WordsA <-> B
ProgrammingA <-> B
MathematicalA ↔ B
AlgebraA ↔ B
LaTeXA \leftrightarrow B
XNOR(A, B) = A <-> B XNOR(A, B) = A <-> B A B lhsPRIMARY rhs XNOR ↔
XNOR(A, B) = A <-> B XNOR(A, B) = A <-> B A B lhsPRIMARY rhs XNOR ↔

The common slip

Expecting XNOR to be “not both”. That is NAND. XNOR is “the same value”; its false rows are the ones where the inputs differ.

Questions

Why does the engine print XNOR(A, B) rather than A <-> B?

It prints what you wrote. The gate form and the connective form are both accepted and both print as themselves; the law says they are equivalent, and the normal-form converter applies it as its first step.

Related

Lesson that teaches this

Tools

See also

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.