Theorem axorbciffatcxorb

Description: Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ). (Contributed by Jarvin Udandy, 7-Sep-2016)

	Ref	Expression
Hypotheses	axorbciffatcxorb.1	|- ( ph \/_ ps )
	axorbciffatcxorb.2	|- ( ch <-> ph )
Assertion	axorbciffatcxorb	|- ( ch \/_ ps )

Proof

Step	Hyp	Ref	Expression
1		axorbciffatcxorb.1	|- ( ph \/_ ps )
2		axorbciffatcxorb.2	|- ( ch <-> ph )
3	1	axorbtnotaiffb	|- -. ( ph <-> ps )
4		xor3	|- ( -. ( ph <-> ps ) <-> ( ph <-> -. ps ) )
5	3 4	mpbi	|- ( ph <-> -. ps )
6	5 2	aiffnbandciffatnotciffb	|- -. ( ch <-> ps )
7		df-xor	|- ( ( ch \/_ ps ) <-> -. ( ch <-> ps ) )
8	6 7	mpbir	|- ( ch \/_ ps )