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 46749
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 206  wfal 1549
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 207
This theorem is referenced by:  mdandyv0  46798  mdandyv1  46799  mdandyv2  46800  mdandyv3  46801  mdandyv4  46802  mdandyv5  46803  mdandyv6  46804  mdandyv7  46805  mdandyv8  46806  mdandyv9  46807  mdandyv10  46808  mdandyv11  46809  mdandyv12  46810  mdandyv13  46811  mdandyv14  46812  dandysum2p2e4  46847
  Copyright terms: Public domain W3C validator