Theorem 3eqtr4rd 2124

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr4rd

Step	Hyp	Ref	Expression
1		3eqtr4d.3	. . 3 |- ( ph -> D = B )
2		3eqtr4d.1	. . 3 |- ( ph -> A = B )
3	1, 2	eqtr4d 2116	. 2 |- ( ph -> D = A )
4		3eqtr4d.2	. 2 |- ( ph -> C = A )
5	3, 4	eqtr4d 2116	1 |- ( ph -> D = C )

Syntax hints:   -> wi 4   = wceq 1284

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-17 1459  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074

This theorem is referenced by:  csbcnvg  4537  phplem4  6341  phplem4on  6353  recexnq  6580  prarloclemcalc  6692  addcomprg  6768  mulcomprg  6770  mulcmpblnrlemg  6917  axmulass  7039  divnegap  7794  modqlt  9335  modqmulnn  9344  iseqcaopr3  9460  ibcval5  9690  cjreb  9753  recj  9754  imcj  9762  imval2  9781  resqrexlemover  9896  sqrtmul  9921  amgm2  10004  maxabslemab  10092  flodddiv4  10334  dfgcd3  10399  absmulgcd  10406  sqpweven  10553  2sqpwodd  10554