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

Proof

Step	Hyp	Ref	Expression
1		abnotbtaxb.1	|- ph
2		abnotbtaxb.2	|- -. ps
3		xor3	|- ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) )
4		pm5.1	|- ( ( ph /\ -. ps ) -> ( ph <-> -. ps ) )
5		ibibr	|- ( ( ( ph /\ -. ps ) -> ( ph <-> -. ps ) ) <-> ( ( ph /\ -. ps ) -> ( ( ph <-> -. ps ) <-> ( ph /\ -. ps ) ) ) )
6	4 5	mpbi	|- ( ( ph /\ -. ps ) -> ( ( ph <-> -. ps ) <-> ( ph /\ -. ps ) ) )
7	1 2 6	mp2an	|- ( ( ph <-> -. ps ) <-> ( ph /\ -. ps ) )
8	3 7	bitri	|- ( -. ( ph <-> ps ) <-> ( ph /\ -. ps ) )
9	1 2 8	mpbir2an	|- -. ( ph <-> ps )
10		df-xor	|- ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )
11	9 10	mpbir	|- ( ph \/_ ps )