Theorem bothfbothsame 47370

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

Syntax hints:   ↔ wb 207  ⊥wfal 1559

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 208

This theorem is referenced by:  mdandyv0  47419  mdandyv1  47420  mdandyv2  47421  mdandyv3  47422  mdandyv4  47423  mdandyv5  47424  mdandyv6  47425  mdandyv7  47426  mdandyv8  47427  mdandyv9  47428  mdandyv10  47429  mdandyv11  47430  mdandyv12  47431  mdandyv13  47432  mdandyv14  47433  dandysum2p2e4  47468