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	|- -. ph
	abnotataxb.2	|- ps
Assertion	abnotataxb	|- ( ph \/_ ps )

Proof

Step	Hyp	Ref	Expression
1		abnotataxb.1	|- -. ph
2		abnotataxb.2	|- ps
3	2 1	pm3.2i	|- ( ps /\ -. ph )
4	3	olci	|- ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) )
5		xor	|- ( -. ( ph <-> ps ) <-> ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) )
6	4 5	mpbir	|- -. ( ph <-> ps )
7		df-xor	|- ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )
8	6 7	mpbir	|- ( ph \/_ ps )