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 
|- ( ( ph <-> ps ) <-> -. ( ph \/_ ps ) )

Proof

Step Hyp Ref Expression
1 df-xor 
 |-  ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )
2 1 con2bii 
 |-  ( ( ph <-> ps ) <-> -. ( ph \/_ ps ) )