Theorem bothtbothsame 47359

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 1543

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  47410  mdandyv2  47411  mdandyv3  47412  mdandyv4  47413  mdandyv5  47414  mdandyv6  47415  mdandyv7  47416  mdandyv8  47417  mdandyv9  47418  mdandyv10  47419  mdandyv11  47420  mdandyv12  47421  mdandyv13  47422  mdandyv14  47423  mdandyv15  47424  dandysum2p2e4  47458