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

Theorem bothtbothsame 38480
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 1444
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  38532  mdandyv2  38533  mdandyv3  38534  mdandyv4  38535  mdandyv5  38536  mdandyv6  38537  mdandyv7  38538  mdandyv8  38539  mdandyv9  38540  mdandyv10  38541  mdandyv11  38542  mdandyv12  38543  mdandyv13  38544  mdandyv14  38545  mdandyv15  38546  dandysum2p2e4  38580
  Copyright terms: Public domain W3C validator