Theorem bothfbothsame 47454

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 1571

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  47503  mdandyv1  47504  mdandyv2  47505  mdandyv3  47506  mdandyv4  47507  mdandyv5  47508  mdandyv6  47509  mdandyv7  47510  mdandyv8  47511  mdandyv9  47512  mdandyv10  47513  mdandyv11  47514  mdandyv12  47515  mdandyv13  47516  mdandyv14  47517  dandysum2p2e4  47552