Theorem 3eqtr4g 2290

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 |- C = A
2		3eqtr4g.1	. . 3 |- ( ph -> A = B )
3	1, 2	eqtrid 2277	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	eqtr4di 2283	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  rabbidva2  2796  rabeqf  2802  csbeq1  3140  csbeq2  3161  csbeq2d  3162  csbnestgf  3190  difeq1  3329  difeq2  3330  uneq2  3366  ineq2  3413  dfrab3ss  3496  ifeq1  3621  ifeq2  3622  ifbi  3639  pweq  3668  sneq  3693  csbsng  3743  rabsn  3749  preq1  3761  preq2  3762  tpeq1  3770  tpeq2  3771  tpeq3  3772  prprc1  3793  opeq1  3876  opeq2  3877  oteq1  3885  oteq2  3886  oteq3  3887  csbunig  3915  unieq  3916  inteq  3945  iineq1  3998  iineq2  4001  dfiin2g  4017  iinrabm  4047  iinin1m  4054  iinxprg  4059  opabbid  4168  mpteq12f  4183  suceq  4514  xpeq1  4754  xpeq2  4755  csbxpg  4822  csbdmg  4941  rneq  4975  reseq1  5023  reseq2  5024  csbresg  5032  resindm  5071  resmpt  5077  resmptf  5079  imaeq1  5087  imaeq2  5088  mptcnv  5156  csbrng  5215  dmpropg  5226  rnpropg  5233  cores  5257  cores2  5266  xpcom  5300  iotaeq  5312  iotabi  5313  fntpg  5403  funimaexg  5431  fveq1  5660  fveq2  5661  fvres  5685  csbfv12g  5701  fnimapr  5728  fndmin  5776  fprg  5858  fsnunfv  5876  fsnunres  5877  fliftf  5963  isoini2  5983  riotaeqdv  5995  riotabidv  5996  riotauni  6001  riotabidva  6012  snriota  6026  oveq  6047  oveq1  6048  oveq2  6049  oprabbid  6097  mpoeq123  6103  mpoeq123dva  6105  mpoeq3dva  6108  resmpo  6142  ovres  6185  f1ocnvd  6248  ofeqd  6259  ofeq  6260  ofreq  6261  f1od2  6422  ovtposg  6481  recseq  6528  tfr2a  6543  rdgeq1  6593  rdgeq2  6594  freceq1  6614  freceq2  6615  eceq1  6793  eceq2  6795  qseq1  6808  qseq2  6809  uniqs  6818  ecinxp  6835  qsinxp  6836  erovlem  6852  ixpeq1  6935  supeq1  7268  supeq2  7271  supeq3  7272  supeq123d  7273  infeq1  7293  infeq2  7296  infeq3  7297  infeq123d  7298  infisoti  7314  djueq12  7321  acneq  7500  addpiord  7619  mulpiord  7620  00sr  8072  negeq  8454  csbnegg  8459  negsubdi  8517  mulneg1  8656  deceq1  9699  deceq2  9700  xnegeq  10146  fseq1p1m1  10414  frec2uzsucd  10749  frec2uzrdg  10757  frecuzrdgsuc  10762  frecuzrdgg  10764  frecuzrdgsuctlem  10771  seqeq1  10798  seqeq2  10799  seqeq3  10800  seqvalcd  10809  seq3f1olemp  10863  hashprg  11158  s1eq  11285  s1prc  11289  s2eqd  11440  s3eqd  11441  s4eqd  11442  s5eqd  11443  s6eqd  11444  s7eqd  11445  s8eqd  11446  shftdm  11485  resqrexlemfp1  11672  negfi  11891  sumeq1  12018  sumeq2  12022  zsumdc  12048  isumss2  12057  fsumsplitsnun  12083  isumclim3  12087  fisumcom2  12102  isumshft  12154  prodeq1f  12216  prodeq2w  12220  prodeq2  12221  zproddc  12243  fprodm1s  12265  fprodp1s  12266  fprodcom2fi  12290  fprodsplitf  12296  ege2le3  12335  efgt1p2  12359  dfphi2  12895  prmdiveq  12911  pceulem  12970  sloteq  13191  setsslid  13237  ressval2  13253  ecqusaddd  13929  ringidvalg  14079  zrhpropd  14746  metreslem  15215  comet  15334  cnmetdval  15364  dvmptfsum  15560  dvply1  15600  lgsdi  15880  lgseisenlem2  15914  lgsquadlem3  15922  uhgrvtxedgiedgb  16108  usgredg2v  16189  depindlem1  16471  redcwlpolemeq1  16809