Theorem bothtbothsame 43933

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
bothtbothsame.1	⊢ (𝜑 ↔ ⊤)
bothtbothsame.2	⊢ (𝜓 ↔ ⊤)

Assertion

Ref	Expression
bothtbothsame	⊢ (𝜑 ↔ 𝜓)

Proof of Theorem bothtbothsame

Step	Hyp	Ref	Expression
1		bothtbothsame.1	. 2 ⊢ (𝜑 ↔ ⊤)
2		bothtbothsame.2	. 2 ⊢ (𝜓 ↔ ⊤)
3	1, 2	bitr4i 281	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 209  ⊤wtru 1543

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:  mdandyv1  43984  mdandyv2  43985  mdandyv3  43986  mdandyv4  43987  mdandyv5  43988  mdandyv6  43989  mdandyv7  43990  mdandyv8  43991  mdandyv9  43992  mdandyv10  43993  mdandyv11  43994  mdandyv12  43995  mdandyv13  43996  mdandyv14  43997  mdandyv15  43998  dandysum2p2e4  44032