Theorem axorbciffatcxorb 41072

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.)

Hypotheses

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

Assertion

Ref	Expression
axorbciffatcxorb	|- ( ch \/_ ps )

Proof of Theorem axorbciffatcxorb

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

Syntax hints:   -. wn 3   <-> wb 196   \/_ wxo 1464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-xor 1465

This theorem is referenced by:  mdandyvrx0  41148  mdandyvrx1  41149  mdandyvrx2  41150  mdandyvrx3  41151  mdandyvrx4  41152  mdandyvrx5  41153  mdandyvrx6  41154  mdandyvrx7  41155