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  7326  supeq2  7329  supeq3  7330  supeq123d  7331  infeq1  7351  infeq2  7354  infeq3  7355  infeq123d  7356  infisoti  7372  djueq12  7379  acneq  7558  addpiord  7683  mulpiord  7684  00sr  8136  negeq  8520  csbnegg  8525  negsubdi  8583  mulneg1  8723  deceq1  9785  deceq2  9786  xnegeq  10239  fseq1p1m1  10511  frec2uzsucd  10851  frec2uzrdg  10859  frecuzrdgsuc  10864  frecuzrdgg  10866  frecuzrdgsuctlem  10873  seqeq1  10900  seqeq2  10901  seqeq3  10902  seqvalcd  10911  seq3f1olemp  10965  hashprg  11263  s1eq  11401  s1prc  11405  s2eqd  11556  s3eqd  11557  s4eqd  11558  s5eqd  11559  s6eqd  11560  s7eqd  11561  s8eqd  11562  shftdm  11601  resqrexlemfp1  11789  negfi  12009  sumeq1  12137  sumeq2  12141  zsumdc  12167  isumss2  12176  fsumsplitsnun  12202  isumclim3  12206  fisumcom2  12221  isumshft  12273  prodeq1f  12335  prodeq2w  12339  prodeq2  12340  zproddc  12362  fprodm1s  12384  fprodp1s  12385  fprodcom2fi  12409  fprodsplitf  12415  ege2le3  12454  efgt1p2  12478  dfphi2  13018  prmdiveq  13034  pceulem  13093  sloteq  13406  setsslid  13452  ressval2  13469  ecqusaddd  14090  gsumzfi  14207  gsumsubmclfi  14212  ringidvalg  14313  zrhpropd  15010  ressascl  15088  asclpropd  15089  metreslem  15530  comet  15649  cnmetdval  15679  dvmptfsum  15875  dvply1  15915  lgsdi  16254  lgseisenlem2  16288  lgsquadlem3  16296  uhgrvtxedgiedgb  16482  usgredg2v  16563  depindlem1  16845  redcwlpolemeq1  17202