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 45610
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 278 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  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 206
This theorem is referenced by:  mdandyv0  45659  mdandyv1  45660  mdandyv2  45661  mdandyv3  45662  mdandyv4  45663  mdandyv5  45664  mdandyv6  45665  mdandyv7  45666  mdandyv8  45667  mdandyv9  45668  mdandyv10  45669  mdandyv11  45670  mdandyv12  45671  mdandyv13  45672  mdandyv14  45673  dandysum2p2e4  45708
  Copyright terms: Public domain W3C validator