Theorem bothtbothsame 39715

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

Syntax hints:   ↔ wb 195  ⊤wtru 1476

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 196

This theorem is referenced by:  mdandyv1  39766  mdandyv2  39767  mdandyv3  39768  mdandyv4  39769  mdandyv5  39770  mdandyv6  39771  mdandyv7  39772  mdandyv8  39773  mdandyv9  39774  mdandyv10  39775  mdandyv11  39776  mdandyv12  39777  mdandyv13  39778  mdandyv14  39779  mdandyv15  39780  dandysum2p2e4  39814