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

Theorem bothfbothsame 27868
Description: Given both a,b are equivalent to F., there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
Hypotheses
Ref Expression
bothfbothsame.1  |-  ( ph  <->  F.  )
bothfbothsame.2  |-  ( ps  <->  F.  )
Assertion
Ref Expression
bothfbothsame  |-  ( ph  <->  ps )

Proof of Theorem bothfbothsame
StepHypRef Expression
1 bothfbothsame.1 . . . . 5  |-  ( ph  <->  F.  )
21aisfina 27866 . . . 4  |-  -.  ph
3 bothfbothsame.2 . . . . 5  |-  ( ps  <->  F.  )
43aisfina 27866 . . . 4  |-  -.  ps
52, 4pm3.2i 441 . . 3  |-  ( -. 
ph  /\  -.  ps )
6 pm5.1 830 . . 3  |-  ( ( -.  ph  /\  -.  ps )  ->  ( -.  ph  <->  -. 
ps ) )
75, 6ax-mp 8 . 2  |-  ( -. 
ph 
<->  -.  ps )
8 notbi 286 . . . 4  |-  ( (
ph 
<->  ps )  <->  ( -.  ph  <->  -. 
ps ) )
9 bicom 191 . . . . 5  |-  ( ( ( ph  <->  ps )  <->  ( -.  ph  <->  -.  ps )
)  <->  ( ( -. 
ph 
<->  -.  ps )  <->  ( ph  <->  ps ) ) )
109biimpi 186 . . . 4  |-  ( ( ( ph  <->  ps )  <->  ( -.  ph  <->  -.  ps )
)  ->  ( ( -.  ph  <->  -.  ps )  <->  (
ph 
<->  ps ) ) )
118, 10ax-mp 8 . . 3  |-  ( ( -.  ph  <->  -.  ps )  <->  (
ph 
<->  ps ) )
1211biimpi 186 . 2  |-  ( ( -.  ph  <->  -.  ps )  ->  ( ph  <->  ps )
)
137, 12ax-mp 8 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    /\ wa 358    F. wfal 1308
This theorem is referenced by:  mdandyv0  27894  mdandyv1  27895  mdandyv2  27896  mdandyv3  27897  mdandyv4  27898  mdandyv5  27899  mdandyv6  27900  mdandyv7  27901  mdandyv8  27902  mdandyv9  27903  mdandyv10  27904  mdandyv11  27905  mdandyv12  27906  mdandyv13  27907  mdandyv14  27908  dandysum2p2e4  27943
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-an 360  df-tru 1310  df-fal 1311
  Copyright terms: Public domain W3C validator