Theorem abnotbtaxb

Description: Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016)

	Ref	Expression
Hypotheses	abnotbtaxb.1	$$⊢\phi$$
	abnotbtaxb.2	$$⊢\neg \psi$$
Assertion	abnotbtaxb	$$⊢\left(\phi ⊻\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		abnotbtaxb.1	$$⊢\phi$$
2		abnotbtaxb.2	$$⊢\neg \psi$$
3		xor3	$$⊢\neg \left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\phi \leftrightarrow \neg \psi \right)$$
4		pm5.1	$$⊢\left(\phi \wedge \neg \psi \right)\to \left(\phi \leftrightarrow \neg \psi \right)$$
5		ibibr	$$⊢\left(\left(\phi \wedge \neg \psi \right)\to \left(\phi \leftrightarrow \neg \psi \right)\right)\leftrightarrow \left(\left(\phi \wedge \neg \psi \right)\to \left(\left(\phi \leftrightarrow \neg \psi \right)\leftrightarrow \left(\phi \wedge \neg \psi \right)\right)\right)$$
6	4 5	mpbi	$$⊢\left(\phi \wedge \neg \psi \right)\to \left(\left(\phi \leftrightarrow \neg \psi \right)\leftrightarrow \left(\phi \wedge \neg \psi \right)\right)$$
7	1 2 6	mp2an	$$⊢\left(\phi \leftrightarrow \neg \psi \right)\leftrightarrow \left(\phi \wedge \neg \psi \right)$$
8	3 7	bitri	$$⊢\neg \left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\phi \wedge \neg \psi \right)$$
9	1 2 8	mpbir2an	$$⊢\neg \left(\phi \leftrightarrow \psi \right)$$
10		df-xor	$$⊢\left(\phi ⊻\psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \psi \right)$$
11	9 10	mpbir	$$⊢\left(\phi ⊻\psi \right)$$