Theorem bothfbothsame 44395

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

Syntax hints:   ↔ wb 205  ⊥wfal 1551

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 206

This theorem is referenced by:  mdandyv0  44444  mdandyv1  44445  mdandyv2  44446  mdandyv3  44447  mdandyv4  44448  mdandyv5  44449  mdandyv6  44450  mdandyv7  44451  mdandyv8  44452  mdandyv9  44453  mdandyv10  44454  mdandyv11  44455  mdandyv12  44456  mdandyv13  44457  mdandyv14  44458  dandysum2p2e4  44493