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 45209
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  45258  mdandyv1  45259  mdandyv2  45260  mdandyv3  45261  mdandyv4  45262  mdandyv5  45263  mdandyv6  45264  mdandyv7  45265  mdandyv8  45266  mdandyv9  45267  mdandyv10  45268  mdandyv11  45269  mdandyv12  45270  mdandyv13  45271  mdandyv14  45272  dandysum2p2e4  45307
  Copyright terms: Public domain W3C validator