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

Theorem bothfbothsame 27743
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 . 2  |-  ( ph  <->  F.  )
2 bothfbothsame.2 . 2  |-  ( ps  <->  F.  )
31, 2bitr4i 244 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    F. wfal 1323
This theorem is referenced by:  mdandyv0  27769  mdandyv1  27770  mdandyv2  27771  mdandyv3  27772  mdandyv4  27773  mdandyv5  27774  mdandyv6  27775  mdandyv7  27776  mdandyv8  27777  mdandyv9  27778  mdandyv10  27779  mdandyv11  27780  mdandyv12  27781  mdandyv13  27782  mdandyv14  27783  dandysum2p2e4  27818
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 178
  Copyright terms: Public domain W3C validator