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 44395
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 277 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wfal 1551
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  44444  mdandyv1  44445  mdandyv2  44446  mdandyv3  44447  mdandyv4  44448  mdandyv5  44449  mdandyv6  44450  mdandyv7  44451  mdandyv8  44452  mdandyv9  44453  mdandyv10  44454  mdandyv11  44455  mdandyv12  44456  mdandyv13  44457  mdandyv14  44458  dandysum2p2e4  44493
  Copyright terms: Public domain W3C validator