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 φ ψ
Assertion aisbnaxb ¬ φ ψ

Proof

Step Hyp Ref Expression
1 aisbnaxb.1 φ ψ
2 1 notnoti ¬ ¬ φ ψ
3 df-xor φ ψ ¬ φ ψ
4 2 3 mtbir ¬ φ ψ