Theorem bothtbothsame 46340

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

Syntax hints:   ↔ wb 205  ⊤wtru 1534

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:  mdandyv1  46391  mdandyv2  46392  mdandyv3  46393  mdandyv4  46394  mdandyv5  46395  mdandyv6  46396  mdandyv7  46397  mdandyv8  46398  mdandyv9  46399  mdandyv10  46400  mdandyv11  46401  mdandyv12  46402  mdandyv13  46403  mdandyv14  46404  mdandyv15  46405  dandysum2p2e4  46439