Theorem 3eqtr4g 2254

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

Syntax hints:   -> wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  rabbidva2  2750  rabeqf  2753  csbeq1  3087  csbeq2  3108  csbeq2d  3109  csbnestgf  3137  difeq1  3275  difeq2  3276  uneq2  3312  ineq2  3359  dfrab3ss  3442  ifeq1  3565  ifeq2  3566  ifbi  3582  pweq  3609  sneq  3634  csbsng  3684  rabsn  3690  preq1  3700  preq2  3701  tpeq1  3709  tpeq2  3710  tpeq3  3711  prprc1  3731  opeq1  3809  opeq2  3810  oteq1  3818  oteq2  3819  oteq3  3820  csbunig  3848  unieq  3849  inteq  3878  iineq1  3931  iineq2  3934  dfiin2g  3950  iinrabm  3980  iinin1m  3987  iinxprg  3992  opabbid  4099  mpteq12f  4114  suceq  4438  xpeq1  4678  xpeq2  4679  csbxpg  4745  csbdmg  4861  rneq  4894  reseq1  4941  reseq2  4942  csbresg  4950  resindm  4989  resmpt  4995  resmptf  4997  imaeq1  5005  imaeq2  5006  mptcnv  5073  csbrng  5132  dmpropg  5143  rnpropg  5150  cores  5174  cores2  5183  xpcom  5217  iotaeq  5228  iotabi  5229  fntpg  5315  funimaexg  5343  fveq1  5560  fveq2  5561  fvres  5585  csbfv12g  5599  fnimapr  5624  fndmin  5672  fprg  5748  fsnunfv  5766  fsnunres  5767  fliftf  5849  isoini2  5869  riotaeqdv  5881  riotabidv  5882  riotauni  5887  riotabidva  5897  snriota  5910  oveq  5931  oveq1  5932  oveq2  5933  oprabbid  5979  mpoeq123  5985  mpoeq123dva  5987  mpoeq3dva  5990  resmpo  6024  ovres  6067  f1ocnvd  6129  ofeqd  6141  ofeq  6142  ofreq  6143  f1od2  6302  ovtposg  6326  recseq  6373  tfr2a  6388  rdgeq1  6438  rdgeq2  6439  freceq1  6459  freceq2  6460  eceq1  6636  eceq2  6638  qseq1  6651  qseq2  6652  uniqs  6661  ecinxp  6678  qsinxp  6679  erovlem  6695  ixpeq1  6777  supeq1  7061  supeq2  7064  supeq3  7065  supeq123d  7066  infeq1  7086  infeq2  7089  infeq3  7090  infeq123d  7091  infisoti  7107  djueq12  7114  acneq  7287  addpiord  7402  mulpiord  7403  00sr  7855  negeq  8238  csbnegg  8243  negsubdi  8301  mulneg1  8440  deceq1  9480  deceq2  9481  xnegeq  9921  fseq1p1m1  10188  frec2uzsucd  10512  frec2uzrdg  10520  frecuzrdgsuc  10525  frecuzrdgg  10527  frecuzrdgsuctlem  10534  seqeq1  10561  seqeq2  10562  seqeq3  10563  seqvalcd  10572  seq3f1olemp  10626  hashprg  10919  shftdm  11006  resqrexlemfp1  11193  negfi  11412  sumeq1  11539  sumeq2  11543  zsumdc  11568  isumss2  11577  fsumsplitsnun  11603  isumclim3  11607  fisumcom2  11622  isumshft  11674  prodeq1f  11736  prodeq2w  11740  prodeq2  11741  zproddc  11763  fprodm1s  11785  fprodp1s  11786  fprodcom2fi  11810  fprodsplitf  11816  ege2le3  11855  efgt1p2  11879  dfphi2  12415  prmdiveq  12431  pceulem  12490  sloteq  12710  setsslid  12756  ressval2  12771  ecqusaddd  13446  ringidvalg  13595  zrhpropd  14260  metreslem  14724  comet  14843  cnmetdval  14873  dvmptfsum  15069  dvply1  15109  lgsdi  15386  lgseisenlem2  15420  lgsquadlem3  15428  redcwlpolemeq1  15811