Metamath Proof Explorer


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 ( 𝜑𝜓 )
axorbciffatcxorb.2 ( 𝜒𝜑 )
Assertion axorbciffatcxorb ( 𝜒𝜓 )

Proof

Step Hyp Ref Expression
1 axorbciffatcxorb.1 ( 𝜑𝜓 )
2 axorbciffatcxorb.2 ( 𝜒𝜑 )
3 1 axorbtnotaiffb ¬ ( 𝜑𝜓 )
4 xor3 ( ¬ ( 𝜑𝜓 ) ↔ ( 𝜑 ↔ ¬ 𝜓 ) )
5 3 4 mpbi ( 𝜑 ↔ ¬ 𝜓 )
6 5 2 aiffnbandciffatnotciffb ¬ ( 𝜒𝜓 )
7 df-xor ( ( 𝜒𝜓 ) ↔ ¬ ( 𝜒𝜓 ) )
8 6 7 mpbir ( 𝜒𝜓 )