Theorem bothtbothsame 38205

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 1439

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  38257  mdandyv2  38258  mdandyv3  38259  mdandyv4  38260  mdandyv5  38261  mdandyv6  38262  mdandyv7  38263  mdandyv8  38264  mdandyv9  38265  mdandyv10  38266  mdandyv11  38267  mdandyv12  38268  mdandyv13  38269  mdandyv14  38270  mdandyv15  38271  dandysum2p2e4  38305