Theorem bothfbothsame 41490

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 1601

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  41539  mdandyv1  41540  mdandyv2  41541  mdandyv3  41542  mdandyv4  41543  mdandyv5  41544  mdandyv6  41545  mdandyv7  41546  mdandyv8  41547  mdandyv9  41548  mdandyv10  41549  mdandyv11  41550  mdandyv12  41551  mdandyv13  41552  mdandyv14  41553  dandysum2p2e4  41588