Theorem 3eqtr4rd 1510

Description: A deduction from three chained equalities.

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 1502	. 2 |- (ph -> D = A)
4		3eqtr4d.2	. 2 |- (ph -> C = A)
5	3, 4	eqtr4d 1502	1 |- (ph -> D = C)

Syntax hints:   -> wi 3   = wceq 953

This theorem is referenced by:  odi 4194  phplem4 4491  divnegt 5730  expp1t 6506  expaddt 6527  expword2it 6536  imcjt 6754  cj11t 6765  abscjt 6769  cjdiv 6826  fsumrev 6967  fsummulc1 6971  serzrelem 6999  bcxmas 7014  geolimilem 7170  absef01tllem 7328  absefm1le 7352  cos2tt 7405  cos01bndlem3 7413  demoivre 7426  clsval2 7627  addinv 8065  vsfval 8194  ip1cnilem6 8312  0lno 8382  nmblolbii 8390  ipasslem5 8425  efimpi 8615  hvsubidt 8816  honegsub 9639  unopf1ot 9756  kbpjt 9796  cnlnadjlem2 9916  adjbdlnt 9931  nmopco 9942  branmfnt 9951  pjtot 10017  cayleylem2 10317  2wsms 10474

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462

Copyright terms: Public domain