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

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

Proof of Theorem bothtbothsame
StepHypRef Expression
1 bothtbothsame.1 . 2  |-  ( ph  <-> T.  )
2 bothtbothsame.2 . 2  |-  ( ps  <-> T.  )
31, 2bitr4i 256 1  |-  ( ph  <->  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188   T. wtru 1439
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 189
This theorem is referenced by:  mdandyv1  38257  mdandyv2  38258  mdandyv3  38259  mdandyv4  38260  mdandyv5  38261  mdandyv6  38262  mdandyv7  38263  mdandyv8  38264  mdandyv9  38265  mdandyv10  38266  mdandyv11  38267  mdandyv12  38268  mdandyv13  38269  mdandyv14  38270  mdandyv15  38271  dandysum2p2e4  38305
  Copyright terms: Public domain W3C validator