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

Theorem bothfbothsame 43934
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
bothfbothsame.1 (𝜑 ↔ ⊥)
bothfbothsame.2 (𝜓 ↔ ⊥)
Assertion
Ref Expression
bothfbothsame (𝜑𝜓)

Proof of Theorem bothfbothsame
StepHypRef Expression
1 bothfbothsame.1 . 2 (𝜑 ↔ ⊥)
2 bothfbothsame.2 . 2 (𝜓 ↔ ⊥)
31, 2bitr4i 281 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wfal 1554
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 210
This theorem is referenced by:  mdandyv0  43983  mdandyv1  43984  mdandyv2  43985  mdandyv3  43986  mdandyv4  43987  mdandyv5  43988  mdandyv6  43989  mdandyv7  43990  mdandyv8  43991  mdandyv9  43992  mdandyv10  43993  mdandyv11  43994  mdandyv12  43995  mdandyv13  43996  mdandyv14  43997  dandysum2p2e4  44032
  Copyright terms: Public domain W3C validator