Theorem bothtbothsame 47453

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 1560

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  47504  mdandyv2  47505  mdandyv3  47506  mdandyv4  47507  mdandyv5  47508  mdandyv6  47509  mdandyv7  47510  mdandyv8  47511  mdandyv9  47512  mdandyv10  47513  mdandyv11  47514  mdandyv12  47515  mdandyv13  47516  mdandyv14  47517  mdandyv15  47518  dandysum2p2e4  47552