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

Theorem bothfbothsame 27191
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 27189 . . . 4  |-  -.  ph
3 bothfbothsame.2 . . . . 5  |-  ( ps  <->  F.  )
43aisfina 27189 . . . 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 1317
This theorem is referenced by:  mdandyv0  27217  mdandyv1  27218  mdandyv2  27219  mdandyv3  27220  mdandyv4  27221  mdandyv5  27222  mdandyv6  27223  mdandyv7  27224  mdandyv8  27225  mdandyv9  27226  mdandyv10  27227  mdandyv11  27228  mdandyv12  27229  mdandyv13  27230  mdandyv14  27231  dandysum2p2e4  27266
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 1319  df-fal 1320
  Copyright terms: Public domain W3C validator