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 )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used 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  3720  csbsng  3770  rabsn  3776  preq1  3788  preq2  3789  tpeq1  3797  tpeq2  3798  tpeq3  3799  prprc1  3821  opeq1  3904  opeq2  3905  oteq1  3913  oteq2  3914  oteq3  3915  csbunig  3943  unieq  3944  inteq  3973  iineq1  4026  iineq2  4029  dfiin2g  4045  iinrabm  4075  iinin1m  4082  iinxprg  4087  opabbid  4196  mpteq12f  4211  suceq  4547  xpeq1  4788  xpeq2  4789  csbxpg  4856  csbdmg  4975  rneq  5009  reseq1  5057  reseq2  5058  csbresg  5066  resindm  5105  resmpt  5111  resmptf  5113  imaeq1  5121  imaeq2  5122  mptcnv  5190  csbrng  5249  dmpropg  5260  rnpropg  5267  cores  5291  cores2  5300  xpcom  5334  iotaeq  5346  iotabi  5347  fntpg  5437  funimaexg  5465  fveq1  5694  fveq2  5695  fvres  5719  csbfv12g  5736  fnimapr  5763  fndmin  5816  fprg  5898  fsnunfv  5916  fsnunres  5917  fliftf  6005  isoini2  6025  riotaeqdv  6039  riotabidv  6040  riotauni  6045  riotabidva  6056  snriota  6070  oveq  6091  oveq1  6092  oveq2  6093  oprabbid  6141  mpoeq123  6147  mpoeq123dva  6149  mpoeq3dva  6152  resmpo  6186  ovres  6229  f1ocnvd  6292  ofeqd  6304  ofeq  6305  ofreq  6306  f1od2  6471  ovtposg  6530  recseq  6577  tfr2a  6592  rdgeq1  6642  rdgeq2  6643  freceq1  6663  freceq2  6664  eceq1  6842  eceq2  6844  qseq1  6857  qseq2  6858  uniqs  6867  ecinxp  6884  qsinxp  6885  erovlem  6901  ixpeq1  6991  supeq1  7327  supeq2  7330  supeq3  7331  supeq123d  7332  infeq1  7352  infeq2  7355  infeq3  7356  infeq123d  7357  infisoti  7373  djueq12  7380  acneq  7559  addpiord  7684  mulpiord  7685  00sr  8137  negeq  8521  csbnegg  8526  negsubdi  8584  mulneg1  8724  deceq1  9786  deceq2  9787  xnegeq  10240  fseq1p1m1  10512  frec2uzsucd  10853  frec2uzrdg  10861  frecuzrdgsuc  10866  frecuzrdgg  10868  frecuzrdgsuctlem  10875  seqeq1  10902  seqeq2  10903  seqeq3  10904  seqvalcd  10913  seq3f1olemp  10967  hashprg  11265  s1eq  11403  s1prc  11407  s2eqd  11558  s3eqd  11559  s4eqd  11560  s5eqd  11561  s6eqd  11562  s7eqd  11563  s8eqd  11564  shftdm  11603  resqrexlemfp1  11791  negfi  12011  sumeq1  12140  sumeq2  12144  zsumdc  12170  isumss2  12179  fsumsplitsnun  12205  isumclim3  12209  fisumcom2  12224  isumshft  12276  prodeq1f  12338  prodeq2w  12342  prodeq2  12343  zproddc  12365  fprodm1s  12387  fprodp1s  12388  fprodcom2fi  12412  fprodsplitf  12418  ege2le3  12457  efgt1p2  12481  dfphi2  13021  prmdiveq  13037  pceulem  13096  sloteq  13409  setsslid  13455  ressval2  13473  ecqusaddd  14094  gsumzfi  14242  gsumsubmclfi  14247  ringidvalg  14348  zrhpropd  15045  ressascl  15123  asclpropd  15124  metreslem  15572  comet  15691  cnmetdval  15721  dvmptfsum  15917  dvply1  15957  lgsdi  16322  lgseisenlem2  16356  lgsquadlem3  16364  uhgrvtxedgiedgb  16550  usgredg2v  16631  depindlem1  16913  redcwlpolemeq1  17271