Theorem bothfbothsame 47620

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 1582

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  47669  mdandyv1  47670  mdandyv2  47671  mdandyv3  47672  mdandyv4  47673  mdandyv5  47674  mdandyv6  47675  mdandyv7  47676  mdandyv8  47677  mdandyv9  47678  mdandyv10  47679  mdandyv11  47680  mdandyv12  47681  mdandyv13  47682  mdandyv14  47683  dandysum2p2e4  47718