Theorem 3eqtr3a 2262

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 2250	. 2 |- ( ph -> A = D )
5	1, 4	eqtr3d 2240	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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  uneqin  3424  coi2  5200  foima  5505  f1imacnv  5541  fvsnun2  5784  fnsnsplitdc  6593  phplem4  6954  phplem4on  6966  halfnqq  7525  resqrexlemcalc1  11358  absefib  12115  efieq1re  12116  restopnb  14686  cnmpt2t  14798  reeflog  15368  rpcxpsqrt  15427