Theorem bothfbothsame 45255

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 1553

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  45304  mdandyv1  45305  mdandyv2  45306  mdandyv3  45307  mdandyv4  45308  mdandyv5  45309  mdandyv6  45310  mdandyv7  45311  mdandyv8  45312  mdandyv9  45313  mdandyv10  45314  mdandyv11  45315  mdandyv12  45316  mdandyv13  45317  mdandyv14  45318  dandysum2p2e4  45353