Metamath Proof Explorer

Theorem aisbnaxb

Description: Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016)

Ref Expression
Hypothesis aisbnaxb.1 
|- ( ph <-> ps )
Assertion aisbnaxb 
|- -. ( ph \/_ ps )

Proof

Step Hyp Ref Expression
1 aisbnaxb.1 
 |-  ( ph <-> ps )
2 1 notnoti 
 |-  -. -. ( ph <-> ps )
3 df-xor 
 |-  ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )
4 2 3 mtbir 
 |-  -. ( ph \/_ ps )