Theorem bothtbothsame 47369

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

Syntax hints:   ↔ wb 207  ⊤wtru 1548

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 208

This theorem is referenced by:  mdandyv1  47420  mdandyv2  47421  mdandyv3  47422  mdandyv4  47423  mdandyv5  47424  mdandyv6  47425  mdandyv7  47426  mdandyv8  47427  mdandyv9  47428  mdandyv10  47429  mdandyv11  47430  mdandyv12  47431  mdandyv13  47432  mdandyv14  47433  mdandyv15  47434  dandysum2p2e4  47468