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