Theorem bothfbothsame 47493

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

Syntax hints:   ↔ wb 209  ⊥wfal 1575

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 210

This theorem is referenced by:  mdandyv0  47542  mdandyv1  47543  mdandyv2  47544  mdandyv3  47545  mdandyv4  47546  mdandyv5  47547  mdandyv6  47548  mdandyv7  47549  mdandyv8  47550  mdandyv9  47551  mdandyv10  47552  mdandyv11  47553  mdandyv12  47554  mdandyv13  47555  mdandyv14  47556  dandysum2p2e4  47591