Theorem 3eqtr3a 2264

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 2252	. 2 |- ( ph -> A = D )
5	1, 4	eqtr3d 2242	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

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

This theorem is referenced by:  uneqin  3432  coi2  5218  foima  5525  f1imacnv  5561  fvsnun2  5805  fnsnsplitdc  6614  phplem4  6977  phplem4on  6990  halfnqq  7558  resqrexlemcalc1  11440  absefib  12197  efieq1re  12198  restopnb  14768  cnmpt2t  14880  reeflog  15450  rpcxpsqrt  15509