Theorem 3eqtr3a 2227

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

Syntax hints:   -> wi 4   = wceq 1348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163

This theorem is referenced by:  uneqin  3378  coi2  5125  foima  5423  f1imacnv  5457  fvsnun2  5691  fnsnsplitdc  6481  phplem4  6829  phplem4on  6841  halfnqq  7359  resqrexlemcalc1  10965  absefib  11720  efieq1re  11721  restopnb  12934  cnmpt2t  13046  reeflog  13537  rpcxpsqrt  13595