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 45920
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 1541
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  45971  mdandyv2  45972  mdandyv3  45973  mdandyv4  45974  mdandyv5  45975  mdandyv6  45976  mdandyv7  45977  mdandyv8  45978  mdandyv9  45979  mdandyv10  45980  mdandyv11  45981  mdandyv12  45982  mdandyv13  45983  mdandyv14  45984  mdandyv15  45985  dandysum2p2e4  46019
  Copyright terms: Public domain W3C validator