Theorem 3eqtr3a 2295

Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)

Hypotheses

Ref	Expression
3eqtr3a.1	|- A = B
3eqtr3a.2	|- ( ph -> A = C )
3eqtr3a.3	|- ( ph -> B = D )

Assertion

Ref	Expression
3eqtr3a	|- ( ph -> C = D )

Proof of Theorem 3eqtr3a

Step	Hyp	Ref	Expression
1		3eqtr3a.2	. 2 |- ( ph -> A = C )
2		3eqtr3a.1	. . 3 |- A = B
3		3eqtr3a.3	. . 3 |- ( ph -> B = D )
4	2, 3	eqtrid 2283	. 2 |- ( ph -> A = D )
5	1, 4	eqtr3d 2273	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231

This theorem is referenced by:  uneqin  3482  coi2  5299  foima  5615  f1imacnv  5651  fvsnun2  5904  fnsnsplitdc  6768  phplem4  7146  phplem4on  7159  halfnqq  7767  resqrexlemcalc1  11758  absefib  12516  efieq1re  12517  restopnb  15205  cnmpt2t  15317  reeflog  15887  rpcxpsqrt  15947