Theorem bothtbothsame 43155

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

Syntax hints:   ↔ wb 208  ⊤wtru 1538

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 209

This theorem is referenced by:  mdandyv1  43206  mdandyv2  43207  mdandyv3  43208  mdandyv4  43209  mdandyv5  43210  mdandyv6  43211  mdandyv7  43212  mdandyv8  43213  mdandyv9  43214  mdandyv10  43215  mdandyv11  43216  mdandyv12  43217  mdandyv13  43218  mdandyv14  43219  mdandyv15  43220  dandysum2p2e4  43254