Theorem bothfbothsame 43130

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 280	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 208  ⊥wfal 1545

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 209

This theorem is referenced by:  mdandyv0  43179  mdandyv1  43180  mdandyv2  43181  mdandyv3  43182  mdandyv4  43183  mdandyv5  43184  mdandyv6  43185  mdandyv7  43186  mdandyv8  43187  mdandyv9  43188  mdandyv10  43189  mdandyv11  43190  mdandyv12  43191  mdandyv13  43192  mdandyv14  43193  dandysum2p2e4  43228