Metamath Proof Explorer


Theorem xnor

Description: Two ways to write XNOR (exclusive not-or). (Contributed by Mario Carneiro, 4-Sep-2016)

Ref Expression
Assertion xnor φ ψ ¬ φ ψ

Proof

Step Hyp Ref Expression
1 df-xor φ ψ ¬ φ ψ
2 1 con2bii φ ψ ¬ φ ψ