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

Theorem bothtbothsame 27845
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 245 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    T. wtru 1326
This theorem is referenced by:  mdandyv1  27873  mdandyv2  27874  mdandyv3  27875  mdandyv4  27876  mdandyv5  27877  mdandyv6  27878  mdandyv7  27879  mdandyv8  27880  mdandyv9  27881  mdandyv10  27882  mdandyv11  27883  mdandyv12  27884  mdandyv13  27885  mdandyv14  27886  mdandyv15  27887  dandysum2p2e4  27921
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 179
  Copyright terms: Public domain W3C validator