Theorem bothfbothsame 41067

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

Syntax hints:   ↔ wb 196  ⊥wfal 1488

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  41116  mdandyv1  41117  mdandyv2  41118  mdandyv3  41119  mdandyv4  41120  mdandyv5  41121  mdandyv6  41122  mdandyv7  41123  mdandyv8  41124  mdandyv9  41125  mdandyv10  41126  mdandyv11  41127  mdandyv12  41128  mdandyv13  41129  mdandyv14  41130  dandysum2p2e4  41165