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

Theorem bothtbothsame 46204
Description: Given both a, b are equivalent to , there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
Hypotheses
Ref Expression
bothtbothsame.1 (𝜑 ↔ ⊤)
bothtbothsame.2 (𝜓 ↔ ⊤)
Assertion
Ref Expression
bothtbothsame (𝜑𝜓)

Proof of Theorem bothtbothsame
StepHypRef Expression
1 bothtbothsame.1 . 2 (𝜑 ↔ ⊤)
2 bothtbothsame.2 . 2 (𝜓 ↔ ⊤)
31, 2bitr4i 278 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wtru 1535
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 206
This theorem is referenced by:  mdandyv1  46255  mdandyv2  46256  mdandyv3  46257  mdandyv4  46258  mdandyv5  46259  mdandyv6  46260  mdandyv7  46261  mdandyv8  46262  mdandyv9  46263  mdandyv10  46264  mdandyv11  46265  mdandyv12  46266  mdandyv13  46267  mdandyv14  46268  mdandyv15  46269  dandysum2p2e4  46303
  Copyright terms: Public domain W3C validator