Theorem bothtbothsame 47619

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 1571

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  47670  mdandyv2  47671  mdandyv3  47672  mdandyv4  47673  mdandyv5  47674  mdandyv6  47675  mdandyv7  47676  mdandyv8  47677  mdandyv9  47678  mdandyv10  47679  mdandyv11  47680  mdandyv12  47681  mdandyv13  47682  mdandyv14  47683  mdandyv15  47684  dandysum2p2e4  47718