Theorem bothtbothsame 38480

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 256	1 |- ( ph <-> ps )

Syntax hints:   <-> wb 188   T. wtru 1444

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 189

This theorem is referenced by:  mdandyv1  38532  mdandyv2  38533  mdandyv3  38534  mdandyv4  38535  mdandyv5  38536  mdandyv6  38537  mdandyv7  38538  mdandyv8  38539  mdandyv9  38540  mdandyv10  38541  mdandyv11  38542  mdandyv12  38543  mdandyv13  38544  mdandyv14  38545  mdandyv15  38546  dandysum2p2e4  38580