Theorem 3eqtr4g 2289

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 2276	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	eqtr4di 2282	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  rabbidva2  2786  rabeqf  2792  csbeq1  3130  csbeq2  3151  csbeq2d  3152  csbnestgf  3180  difeq1  3318  difeq2  3319  uneq2  3355  ineq2  3402  dfrab3ss  3485  ifeq1  3608  ifeq2  3609  ifbi  3626  pweq  3655  sneq  3680  csbsng  3730  rabsn  3736  preq1  3748  preq2  3749  tpeq1  3757  tpeq2  3758  tpeq3  3759  prprc1  3780  opeq1  3862  opeq2  3863  oteq1  3871  oteq2  3872  oteq3  3873  csbunig  3901  unieq  3902  inteq  3931  iineq1  3984  iineq2  3987  dfiin2g  4003  iinrabm  4033  iinin1m  4040  iinxprg  4045  opabbid  4154  mpteq12f  4169  suceq  4499  xpeq1  4739  xpeq2  4740  csbxpg  4807  csbdmg  4925  rneq  4959  reseq1  5007  reseq2  5008  csbresg  5016  resindm  5055  resmpt  5061  resmptf  5063  imaeq1  5071  imaeq2  5072  mptcnv  5139  csbrng  5198  dmpropg  5209  rnpropg  5216  cores  5240  cores2  5249  xpcom  5283  iotaeq  5295  iotabi  5296  fntpg  5386  funimaexg  5414  fveq1  5638  fveq2  5639  fvres  5663  csbfv12g  5679  fnimapr  5706  fndmin  5754  fprg  5837  fsnunfv  5855  fsnunres  5856  fliftf  5940  isoini2  5960  riotaeqdv  5972  riotabidv  5973  riotauni  5978  riotabidva  5989  snriota  6003  oveq  6024  oveq1  6025  oveq2  6026  oprabbid  6074  mpoeq123  6080  mpoeq123dva  6082  mpoeq3dva  6085  resmpo  6119  ovres  6162  f1ocnvd  6225  ofeqd  6237  ofeq  6238  ofreq  6239  f1od2  6400  ovtposg  6425  recseq  6472  tfr2a  6487  rdgeq1  6537  rdgeq2  6538  freceq1  6558  freceq2  6559  eceq1  6737  eceq2  6739  qseq1  6752  qseq2  6753  uniqs  6762  ecinxp  6779  qsinxp  6780  erovlem  6796  ixpeq1  6878  supeq1  7185  supeq2  7188  supeq3  7189  supeq123d  7190  infeq1  7210  infeq2  7213  infeq3  7214  infeq123d  7215  infisoti  7231  djueq12  7238  acneq  7417  addpiord  7536  mulpiord  7537  00sr  7989  negeq  8372  csbnegg  8377  negsubdi  8435  mulneg1  8574  deceq1  9615  deceq2  9616  xnegeq  10062  fseq1p1m1  10329  frec2uzsucd  10663  frec2uzrdg  10671  frecuzrdgsuc  10676  frecuzrdgg  10678  frecuzrdgsuctlem  10685  seqeq1  10712  seqeq2  10713  seqeq3  10714  seqvalcd  10723  seq3f1olemp  10777  hashprg  11072  s1eq  11196  s1prc  11200  s2eqd  11351  s3eqd  11352  s4eqd  11353  s5eqd  11354  s6eqd  11355  s7eqd  11356  s8eqd  11357  shftdm  11383  resqrexlemfp1  11570  negfi  11789  sumeq1  11916  sumeq2  11920  zsumdc  11946  isumss2  11955  fsumsplitsnun  11981  isumclim3  11985  fisumcom2  12000  isumshft  12052  prodeq1f  12114  prodeq2w  12118  prodeq2  12119  zproddc  12141  fprodm1s  12163  fprodp1s  12164  fprodcom2fi  12188  fprodsplitf  12194  ege2le3  12233  efgt1p2  12257  dfphi2  12793  prmdiveq  12809  pceulem  12868  sloteq  13088  setsslid  13134  ressval2  13150  ecqusaddd  13826  ringidvalg  13976  zrhpropd  14642  metreslem  15106  comet  15225  cnmetdval  15255  dvmptfsum  15451  dvply1  15491  lgsdi  15768  lgseisenlem2  15802  lgsquadlem3  15810  uhgrvtxedgiedgb  15996  usgredg2v  16077  redcwlpolemeq1  16661