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

Theorem axorbciffatcxorb 27976
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 27974 . . . 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 27975 . 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  28029  mdandyvrx1  28030  mdandyvrx2  28031  mdandyvrx3  28032  mdandyvrx4  28033  mdandyvrx5  28034  mdandyvrx6  28035  mdandyvrx7  28036  mdandyvrx8  28037  mdandyvrx9  28038  mdandyvrx10  28039  mdandyvrx11  28040  mdandyvrx12  28041  mdandyvrx13  28042  mdandyvrx14  28043  mdandyvrx15  28044
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