Theorem 3eqtr3a 2289

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  uneqin  3472  coi2  5279  foima  5595  f1imacnv  5631  fvsnun2  5882  fnsnsplitdc  6738  phplem4  7109  phplem4on  7122  halfnqq  7725  resqrexlemcalc1  11699  absefib  12457  efieq1re  12458  restopnb  15046  cnmpt2t  15158  reeflog  15728  rpcxpsqrt  15787