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 41490
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 267 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wfal 1601
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 197
This theorem is referenced by:  mdandyv0  41539  mdandyv1  41540  mdandyv2  41541  mdandyv3  41542  mdandyv4  41543  mdandyv5  41544  mdandyv6  41545  mdandyv7  41546  mdandyv8  41547  mdandyv9  41548  mdandyv10  41549  mdandyv11  41550  mdandyv12  41551  mdandyv13  41552  mdandyv14  41553  dandysum2p2e4  41588
  Copyright terms: Public domain W3C validator