Theorem bothfbothsame 47024

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

Step	Hyp	Ref	Expression
1		bothfbothsame.1	. 2 ⊢ (𝜑 ↔ ⊥)
2		bothfbothsame.2	. 2 ⊢ (𝜓 ↔ ⊥)
3	1, 2	bitr4i 278	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 206  ⊥wfal 1553

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  47073  mdandyv1  47074  mdandyv2  47075  mdandyv3  47076  mdandyv4  47077  mdandyv5  47078  mdandyv6  47079  mdandyv7  47080  mdandyv8  47081  mdandyv9  47082  mdandyv10  47083  mdandyv11  47084  mdandyv12  47085  mdandyv13  47086  mdandyv14  47087  dandysum2p2e4  47122