Theorem bothtbothsame 46814

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 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 207

This theorem is referenced by:  mdandyv1  46865  mdandyv2  46866  mdandyv3  46867  mdandyv4  46868  mdandyv5  46869  mdandyv6  46870  mdandyv7  46871  mdandyv8  46872  mdandyv9  46873  mdandyv10  46874  mdandyv11  46875  mdandyv12  46876  mdandyv13  46877  mdandyv14  46878  mdandyv15  46879  dandysum2p2e4  46913