Theorem bothfbothsame 44282

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  44331  mdandyv1  44332  mdandyv2  44333  mdandyv3  44334  mdandyv4  44335  mdandyv5  44336  mdandyv6  44337  mdandyv7  44338  mdandyv8  44339  mdandyv9  44340  mdandyv10  44341  mdandyv11  44342  mdandyv12  44343  mdandyv13  44344  mdandyv14  44345  dandysum2p2e4  44380