Theorem 3eqtr4g 2296

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

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  rabbidva2  2805  rabeqf  2811  csbeq1  3150  csbeq2  3171  csbeq2d  3172  csbnestgf  3200  difeq1  3340  difeq2  3341  uneq2  3377  ineq2  3426  dfrab3ss  3511  ifeq1  3643  ifeq2  3644  ifbi  3661  pweq  3691  sneq  3719  csbsng  3769  rabsn  3775  preq1  3787  preq2  3788  tpeq1  3796  tpeq2  3797  tpeq3  3798  prprc1  3819  opeq1  3902  opeq2  3903  oteq1  3911  oteq2  3912  oteq3  3913  csbunig  3941  unieq  3942  inteq  3971  iineq1  4024  iineq2  4027  dfiin2g  4043  iinrabm  4073  iinin1m  4080  iinxprg  4085  opabbid  4194  mpteq12f  4209  suceq  4545  xpeq1  4786  xpeq2  4787  csbxpg  4854  csbdmg  4973  rneq  5007  reseq1  5055  reseq2  5056  csbresg  5064  resindm  5103  resmpt  5109  resmptf  5111  imaeq1  5119  imaeq2  5120  mptcnv  5188  csbrng  5247  dmpropg  5258  rnpropg  5265  cores  5289  cores2  5298  xpcom  5332  iotaeq  5344  iotabi  5345  fntpg  5435  funimaexg  5463  fveq1  5692  fveq2  5693  fvres  5717  csbfv12g  5733  fnimapr  5760  fndmin  5810  fprg  5892  fsnunfv  5910  fsnunres  5911  fliftf  5998  isoini2  6018  riotaeqdv  6032  riotabidv  6033  riotauni  6038  riotabidva  6049  snriota  6063  oveq  6084  oveq1  6085  oveq2  6086  oprabbid  6134  mpoeq123  6140  mpoeq123dva  6142  mpoeq3dva  6145  resmpo  6179  ovres  6222  f1ocnvd  6285  ofeqd  6297  ofeq  6298  ofreq  6299  f1od2  6464  ovtposg  6523  recseq  6570  tfr2a  6585  rdgeq1  6635  rdgeq2  6636  freceq1  6656  freceq2  6657  eceq1  6835  eceq2  6837  qseq1  6850  qseq2  6851  uniqs  6860  ecinxp  6877  qsinxp  6878  erovlem  6894  ixpeq1  6984  supeq1  7319  supeq2  7322  supeq3  7323  supeq123d  7324  infeq1  7344  infeq2  7347  infeq3  7348  infeq123d  7349  infisoti  7365  djueq12  7372  acneq  7551  addpiord  7676  mulpiord  7677  00sr  8129  negeq  8512  csbnegg  8517  negsubdi  8575  mulneg1  8715  deceq1  9763  deceq2  9764  xnegeq  10211  fseq1p1m1  10482  frec2uzsucd  10819  frec2uzrdg  10827  frecuzrdgsuc  10832  frecuzrdgg  10834  frecuzrdgsuctlem  10841  seqeq1  10868  seqeq2  10869  seqeq3  10870  seqvalcd  10879  seq3f1olemp  10933  hashprg  11230  s1eq  11368  s1prc  11372  s2eqd  11523  s3eqd  11524  s4eqd  11525  s5eqd  11526  s6eqd  11527  s7eqd  11528  s8eqd  11529  shftdm  11568  resqrexlemfp1  11756  negfi  11975  sumeq1  12102  sumeq2  12106  zsumdc  12132  isumss2  12141  fsumsplitsnun  12167  isumclim3  12171  fisumcom2  12186  isumshft  12238  prodeq1f  12300  prodeq2w  12304  prodeq2  12305  zproddc  12327  fprodm1s  12349  fprodp1s  12350  fprodcom2fi  12374  fprodsplitf  12380  ege2le3  12419  efgt1p2  12443  dfphi2  12979  prmdiveq  12995  pceulem  13054  sloteq  13338  setsslid  13384  ressval2  13400  ecqusaddd  14021  gsumzfi  14138  gsumsubmclfi  14143  ringidvalg  14242  zrhpropd  14936  metreslem  15407  comet  15526  cnmetdval  15556  dvmptfsum  15752  dvply1  15792  lgsdi  16073  lgseisenlem2  16107  lgsquadlem3  16115  uhgrvtxedgiedgb  16301  usgredg2v  16382  depindlem1  16664  redcwlpolemeq1  17012