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

Theorem bothtbothsame 41570
 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 267 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196  ⊤wtru 1631 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 197 This theorem is referenced by:  mdandyv1  41621  mdandyv2  41622  mdandyv3  41623  mdandyv4  41624  mdandyv5  41625  mdandyv6  41626  mdandyv7  41627  mdandyv8  41628  mdandyv9  41629  mdandyv10  41630  mdandyv11  41631  mdandyv12  41632  mdandyv13  41633  mdandyv14  41634  mdandyv15  41635  dandysum2p2e4  41669
 Copyright terms: Public domain W3C validator