Theorem bothfbothsame 47796

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  47845  mdandyv1  47846  mdandyv2  47847  mdandyv3  47848  mdandyv4  47849  mdandyv5  47850  mdandyv6  47851  mdandyv7  47852  mdandyv8  47853  mdandyv9  47854  mdandyv10  47855  mdandyv11  47856  mdandyv12  47857  mdandyv13  47858  mdandyv14  47859  dandysum2p2e4  47894