Theorem bothfbothsame 47788

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

This proof depends on syntax axioms:   ↔ wb 209  ⊥wfal 1582

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mdandyv0  47837  mdandyv1  47838  mdandyv2  47839  mdandyv3  47840  mdandyv4  47841  mdandyv5  47842  mdandyv6  47843  mdandyv7  47844  mdandyv8  47845  mdandyv9  47846  mdandyv10  47847  mdandyv11  47848  mdandyv12  47849  mdandyv13  47850  mdandyv14  47851  dandysum2p2e4  47886