Theorem bothtbothsame 47492

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 1564

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  47543  mdandyv2  47544  mdandyv3  47545  mdandyv4  47546  mdandyv5  47547  mdandyv6  47548  mdandyv7  47549  mdandyv8  47550  mdandyv9  47551  mdandyv10  47552  mdandyv11  47553  mdandyv12  47554  mdandyv13  47555  mdandyv14  47556  mdandyv15  47557  dandysum2p2e4  47591