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 ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )