Theorem 3eqtr4g 2235

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

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  rabbidva2  2726  rabeqf  2729  csbeq1  3062  csbeq2  3083  csbeq2d  3084  csbnestgf  3111  difeq1  3248  difeq2  3249  uneq2  3285  ineq2  3332  dfrab3ss  3415  ifeq1  3539  ifeq2  3540  ifbi  3556  pweq  3580  sneq  3605  csbsng  3655  rabsn  3661  preq1  3671  preq2  3672  tpeq1  3680  tpeq2  3681  tpeq3  3682  prprc1  3702  opeq1  3780  opeq2  3781  oteq1  3789  oteq2  3790  oteq3  3791  csbunig  3819  unieq  3820  inteq  3849  iineq1  3902  iineq2  3905  dfiin2g  3921  iinrabm  3951  iinin1m  3958  iinxprg  3963  opabbid  4070  mpteq12f  4085  suceq  4404  xpeq1  4642  xpeq2  4643  csbxpg  4709  csbdmg  4823  rneq  4856  reseq1  4903  reseq2  4904  csbresg  4912  resindm  4951  resmpt  4957  resmptf  4959  imaeq1  4967  imaeq2  4968  mptcnv  5033  csbrng  5092  dmpropg  5103  rnpropg  5110  cores  5134  cores2  5143  xpcom  5177  iotaeq  5188  iotabi  5189  fntpg  5274  funimaexg  5302  fveq1  5516  fveq2  5517  fvres  5541  csbfv12g  5553  fnimapr  5578  fndmin  5625  fprg  5701  fsnunfv  5719  fsnunres  5720  fliftf  5802  isoini2  5822  riotaeqdv  5834  riotabidv  5835  riotauni  5839  riotabidva  5849  snriota  5862  oveq  5883  oveq1  5884  oveq2  5885  oprabbid  5930  mpoeq123  5936  mpoeq123dva  5938  mpoeq3dva  5941  resmpo  5975  ovres  6016  f1ocnvd  6075  ofeq  6087  ofreq  6088  f1od2  6238  ovtposg  6262  recseq  6309  tfr2a  6324  rdgeq1  6374  rdgeq2  6375  freceq1  6395  freceq2  6396  eceq1  6572  eceq2  6574  qseq1  6585  qseq2  6586  uniqs  6595  ecinxp  6612  qsinxp  6613  erovlem  6629  ixpeq1  6711  supeq1  6987  supeq2  6990  supeq3  6991  supeq123d  6992  infeq1  7012  infeq2  7015  infeq3  7016  infeq123d  7017  infisoti  7033  djueq12  7040  addpiord  7317  mulpiord  7318  00sr  7770  negeq  8152  csbnegg  8157  negsubdi  8215  mulneg1  8354  deceq1  9390  deceq2  9391  xnegeq  9829  fseq1p1m1  10096  frec2uzsucd  10403  frec2uzrdg  10411  frecuzrdgsuc  10416  frecuzrdgg  10418  frecuzrdgsuctlem  10425  seqeq1  10450  seqeq2  10451  seqeq3  10452  seqvalcd  10461  seq3f1olemp  10504  hashprg  10790  shftdm  10833  resqrexlemfp1  11020  negfi  11238  sumeq1  11365  sumeq2  11369  zsumdc  11394  isumss2  11403  fsumsplitsnun  11429  isumclim3  11433  fisumcom2  11448  isumshft  11500  prodeq1f  11562  prodeq2w  11566  prodeq2  11567  zproddc  11589  fprodm1s  11611  fprodp1s  11612  fprodcom2fi  11636  fprodsplitf  11642  ege2le3  11681  efgt1p2  11705  dfphi2  12222  prmdiveq  12238  pceulem  12296  sloteq  12469  setsslid  12515  ressval2  12528  ringidvalg  13149  metreslem  13919  comet  14038  cnmetdval  14068  lgsdi  14477  lgseisenlem2  14490  redcwlpolemeq1  14841