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

Theorem bothtbothsame 27970
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 . . . 4  |-  ( ph  <->  T.  )
21aistia 27968 . . 3  |-  ph
3 bothtbothsame.2 . . . 4  |-  ( ps  <->  T.  )
43aistia 27968 . . 3  |-  ps
52, 4pm3.2i 441 . 2  |-  ( ph  /\ 
ps )
6 pm5.1 830 . 2  |-  ( (
ph  /\  ps )  ->  ( ph  <->  ps )
)
75, 6ax-mp 8 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    T. wtru 1307
This theorem is referenced by:  mdandyv1  27998  mdandyv2  27999  mdandyv3  28000  mdandyv4  28001  mdandyv5  28002  mdandyv6  28003  mdandyv7  28004  mdandyv8  28005  mdandyv9  28006  mdandyv10  28007  mdandyv11  28008  mdandyv12  28009  mdandyv13  28010  mdandyv14  28011  mdandyv15  28012  dandysum2p2e4  28046
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 177  df-an 360  df-tru 1310
  Copyright terms: Public domain W3C validator