Theorem bothfbothsame 39716

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

Syntax hints:   ↔ wb 195  ⊥wfal 1480

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 196

This theorem is referenced by:  mdandyv0  39765  mdandyv1  39766  mdandyv2  39767  mdandyv3  39768  mdandyv4  39769  mdandyv5  39770  mdandyv6  39771  mdandyv7  39772  mdandyv8  39773  mdandyv9  39774  mdandyv10  39775  mdandyv11  39776  mdandyv12  39777  mdandyv13  39778  mdandyv14  39779  dandysum2p2e4  39814