Theorem 3eqtr4d 1134

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
3eqtr4d	|- (ph -> C = D)

Proof of Theorem 3eqtr4d

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

Syntax hints:   -> wi 2   = wceq 1091

This theorem is referenced by:  fnsnfv 2861  frsuc 2991  oasuc 3131  omsuc 3133  oesuc 3134  oaass 3163  nnmsucr 3182  alephcard 3673  addcompi 3816  addasspi 3817  mulcompi 3818  mulasspi 3819  distrpi 3820  adddirt 4103  add23t 4126  addsubasst 4150  mul23t 4176  mulneg2t 4197  negdi3t 4202  divasst 4239  divdiv23t 4271  seqsuclem 4669  expp1t 4678  hvadd23t 5011  hvsub4t 5014  hvaddsub12t 5015  hvaddsubasst 5018  his7 5051  his2subt 5052  hoscom 5605  hosass 5607  hosdir 5609  hoddir 5610  pjsdi 5625  pjddi 5626  pjadjco 5631  pjss2co 5634  pjorthco 5639  pjadj2co 5656  pj3cor1 5661  strlem3a 5693  golem1 5704

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org