Theorem abnotataxb

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

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

Proof

Step	Hyp	Ref	Expression
1		abnotataxb.1	$$⊢\neg \phi$$
2		abnotataxb.2	$$⊢\psi$$
3	2 1	pm3.2i	$$⊢\left(\psi \wedge \neg \phi \right)$$
4	3	olci	$$⊢\left(\left(\phi \wedge \neg \psi \right)\vee \left(\psi \wedge \neg \phi \right)\right)$$
5		xor	$$⊢\neg \left(\phi \leftrightarrow \psi \right)\leftrightarrow \left(\left(\phi \wedge \neg \psi \right)\vee \left(\psi \wedge \neg \phi \right)\right)$$
6	4 5	mpbir	$$⊢\neg \left(\phi \leftrightarrow \psi \right)$$
7		df-xor	$$⊢\left(\phi ⊻\psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \psi \right)$$
8	6 7	mpbir	$$⊢\left(\phi ⊻\psi \right)$$