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

Theorem bothfbothsame 27857
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 245 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    F. wfal 1327
This theorem is referenced by:  mdandyv0  27883  mdandyv1  27884  mdandyv2  27885  mdandyv3  27886  mdandyv4  27887  mdandyv5  27888  mdandyv6  27889  mdandyv7  27890  mdandyv8  27891  mdandyv9  27892  mdandyv10  27893  mdandyv11  27894  mdandyv12  27895  mdandyv13  27896  mdandyv14  27897  dandysum2p2e4  27932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator