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 43013
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 279 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wfal 1540
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 208
This theorem is referenced by:  mdandyv0  43062  mdandyv1  43063  mdandyv2  43064  mdandyv3  43065  mdandyv4  43066  mdandyv5  43067  mdandyv6  43068  mdandyv7  43069  mdandyv8  43070  mdandyv9  43071  mdandyv10  43072  mdandyv11  43073  mdandyv12  43074  mdandyv13  43075  mdandyv14  43076  dandysum2p2e4  43111
  Copyright terms: Public domain W3C validator