Users' Mathboxes Mathbox for Jarvin Udandy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  axorbciffatcxorb Unicode version

Theorem axorbciffatcxorb 27285
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
StepHypRef Expression
1 axorbciffatcxorb.1 . . . . 5  |-  ( ph \/_ ps )
21axorbtnotaiffb 27283 . . . 4  |-  -.  ( ph 
<->  ps )
3 xor3 346 . . . . 5  |-  ( -.  ( ph  <->  ps )  <->  (
ph 
<->  -.  ps ) )
43biimpi 186 . . . 4  |-  ( -.  ( ph  <->  ps )  ->  ( ph  <->  -.  ps )
)
52, 4ax-mp 8 . . 3  |-  ( ph  <->  -. 
ps )
6 axorbciffatcxorb.2 . . 3  |-  ( ch  <->  ph )
75, 6aiffnbandciffatnotciffb 27284 . 2  |-  -.  ( ch 
<->  ps )
8 df-xor 1296 . . . 4  |-  ( ( ch \/_ ps )  <->  -.  ( ch  <->  ps )
)
9 bicom 191 . . . . 5  |-  ( ( ( ch \/_ ps ) 
<->  -.  ( ch  <->  ps )
)  <->  ( -.  ( ch 
<->  ps )  <->  ( ch \/_ ps ) ) )
109biimpi 186 . . . 4  |-  ( ( ( ch \/_ ps ) 
<->  -.  ( ch  <->  ps )
)  ->  ( -.  ( ch  <->  ps )  <->  ( ch \/_ ps ) ) )
118, 10ax-mp 8 . . 3  |-  ( -.  ( ch  <->  ps )  <->  ( ch \/_ ps )
)
1211biimpi 186 . 2  |-  ( -.  ( ch  <->  ps )  ->  ( ch \/_ ps ) )
137, 12ax-mp 8 1  |-  ( ch
\/_ ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   \/_wxo 1295
This theorem is referenced by:  mdandyvrx0  27338  mdandyvrx1  27339  mdandyvrx2  27340  mdandyvrx3  27341  mdandyvrx4  27342  mdandyvrx5  27343  mdandyvrx6  27344  mdandyvrx7  27345  mdandyvrx8  27346  mdandyvrx9  27347  mdandyvrx10  27348  mdandyvrx11  27349  mdandyvrx12  27350  mdandyvrx13  27351  mdandyvrx14  27352  mdandyvrx15  27353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-xor 1296
  Copyright terms: Public domain W3C validator