Theorem bothtbothsame 46870

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

Syntax hints:   ↔ wb 206  ⊤wtru 1541

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 207

This theorem is referenced by:  mdandyv1  46921  mdandyv2  46922  mdandyv3  46923  mdandyv4  46924  mdandyv5  46925  mdandyv6  46926  mdandyv7  46927  mdandyv8  46928  mdandyv9  46929  mdandyv10  46930  mdandyv11  46931  mdandyv12  46932  mdandyv13  46933  mdandyv14  46934  mdandyv15  46935  dandysum2p2e4  46969