Theorem 3eqtr4rd 1518

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

Syntax hints:   -> wi 3   = wceq 956

This theorem is referenced by:  odi 4210  phplem4 4511  divnegt 5774  expp1t 6574  expaddt 6596  expword2it 6605  imcjt 6819  cj11t 6830  abscjt 6834  cjdiv 6888  absmaxt 6897  fsumrev 7029  fsummulc1 7033  serzrelem 7061  bcxmas 7076  geolimilem 7235  absef01tllem 7387  absefm1le 7412  cos2tt 7463  cos01bndlem3 7471  demoivre 7484  clsval2 7685  addinv 8128  vsfval 8254  ip1cnilem6 8378  0lno 8450  nmblolbii 8459  ipasslem5 8494  efimpi 8698  hvsubidt 8895  honegsub 9722  unopf1ot 9840  kbpjt 9880  cnlnadjlem2 10001  adjbdlnt 10016  nmopco 10028  branmfnt 10038  pjtot 10107  cayleylem2 10410  2wsms 10630

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

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

Copyright terms: Public domain