Theorem bothtbothsame 47787

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

This proof depends on syntax axioms:   ↔ wb 209  ⊤wtru 1571

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mdandyv1  47838  mdandyv2  47839  mdandyv3  47840  mdandyv4  47841  mdandyv5  47842  mdandyv6  47843  mdandyv7  47844  mdandyv8  47845  mdandyv9  47846  mdandyv10  47847  mdandyv11  47848  mdandyv12  47849  mdandyv13  47850  mdandyv14  47851  mdandyv15  47852  dandysum2p2e4  47886