Theorem bothfbothsame 47348

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 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 207

This theorem is referenced by:  mdandyv0  47397  mdandyv1  47398  mdandyv2  47399  mdandyv3  47400  mdandyv4  47401  mdandyv5  47402  mdandyv6  47403  mdandyv7  47404  mdandyv8  47405  mdandyv9  47406  mdandyv10  47407  mdandyv11  47408  mdandyv12  47409  mdandyv13  47410  mdandyv14  47411  dandysum2p2e4  47446