Theorem bothtbothsame 41066

Description: Given both a, b are equivalent to T., there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)

Hypotheses

Ref	Expression
bothtbothsame.1	|- ( ph <-> T. )
bothtbothsame.2	|- ( ps <-> T. )

Assertion

Ref	Expression
bothtbothsame	|- ( ph <-> ps )

Proof of Theorem bothtbothsame

Step	Hyp	Ref	Expression
1		bothtbothsame.1	. 2 |- ( ph <-> T. )
2		bothtbothsame.2	. 2 |- ( ps <-> T. )
3	1, 2	bitr4i 267	1 |- ( ph <-> ps )

Syntax hints:   <-> wb 196   T. wtru 1484

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 197

This theorem is referenced by:  mdandyv1  41117  mdandyv2  41118  mdandyv3  41119  mdandyv4  41120  mdandyv5  41121  mdandyv6  41122  mdandyv7  41123  mdandyv8  41124  mdandyv9  41125  mdandyv10  41126  mdandyv11  41127  mdandyv12  41128  mdandyv13  41129  mdandyv14  41130  mdandyv15  41131  dandysum2p2e4  41165