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	$$⊢\phi \leftrightarrow \psi$$
Assertion	aisbnaxb	$$⊢\neg \left(\phi ⊻\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		aisbnaxb.1	$$⊢\phi \leftrightarrow \psi$$
2	1	notnoti	$$⊢\neg \neg \left(\phi \leftrightarrow \psi \right)$$
3		df-xor	$$⊢\left(\phi ⊻\psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \psi \right)$$
4	2 3	mtbir	$$⊢\neg \left(\phi ⊻\psi \right)$$