Theorem bothfbothsame 45910

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 1552

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  45959  mdandyv1  45960  mdandyv2  45961  mdandyv3  45962  mdandyv4  45963  mdandyv5  45964  mdandyv6  45965  mdandyv7  45966  mdandyv8  45967  mdandyv9  45968  mdandyv10  45969  mdandyv11  45970  mdandyv12  45971  mdandyv13  45972  mdandyv14  45973  dandysum2p2e4  46008