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