Theorem 3eqtr4g 2251

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 2238	. 2 |- ( ph -> C = B )
4		3eqtr4g.3	. 2 |- D = B
5	3, 4	eqtr4di 2244	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  rabbidva2  2747  rabeqf  2750  csbeq1  3084  csbeq2  3105  csbeq2d  3106  csbnestgf  3134  difeq1  3271  difeq2  3272  uneq2  3308  ineq2  3355  dfrab3ss  3438  ifeq1  3561  ifeq2  3562  ifbi  3578  pweq  3605  sneq  3630  csbsng  3680  rabsn  3686  preq1  3696  preq2  3697  tpeq1  3705  tpeq2  3706  tpeq3  3707  prprc1  3727  opeq1  3805  opeq2  3806  oteq1  3814  oteq2  3815  oteq3  3816  csbunig  3844  unieq  3845  inteq  3874  iineq1  3927  iineq2  3930  dfiin2g  3946  iinrabm  3976  iinin1m  3983  iinxprg  3988  opabbid  4095  mpteq12f  4110  suceq  4434  xpeq1  4674  xpeq2  4675  csbxpg  4741  csbdmg  4857  rneq  4890  reseq1  4937  reseq2  4938  csbresg  4946  resindm  4985  resmpt  4991  resmptf  4993  imaeq1  5001  imaeq2  5002  mptcnv  5069  csbrng  5128  dmpropg  5139  rnpropg  5146  cores  5170  cores2  5179  xpcom  5213  iotaeq  5224  iotabi  5225  fntpg  5311  funimaexg  5339  fveq1  5554  fveq2  5555  fvres  5579  csbfv12g  5593  fnimapr  5618  fndmin  5666  fprg  5742  fsnunfv  5760  fsnunres  5761  fliftf  5843  isoini2  5863  riotaeqdv  5875  riotabidv  5876  riotauni  5881  riotabidva  5891  snriota  5904  oveq  5925  oveq1  5926  oveq2  5927  oprabbid  5972  mpoeq123  5978  mpoeq123dva  5980  mpoeq3dva  5983  resmpo  6017  ovres  6060  f1ocnvd  6122  ofeqd  6134  ofeq  6135  ofreq  6136  f1od2  6290  ovtposg  6314  recseq  6361  tfr2a  6376  rdgeq1  6426  rdgeq2  6427  freceq1  6447  freceq2  6448  eceq1  6624  eceq2  6626  qseq1  6639  qseq2  6640  uniqs  6649  ecinxp  6666  qsinxp  6667  erovlem  6683  ixpeq1  6765  supeq1  7047  supeq2  7050  supeq3  7051  supeq123d  7052  infeq1  7072  infeq2  7075  infeq3  7076  infeq123d  7077  infisoti  7093  djueq12  7100  addpiord  7378  mulpiord  7379  00sr  7831  negeq  8214  csbnegg  8219  negsubdi  8277  mulneg1  8416  deceq1  9455  deceq2  9456  xnegeq  9896  fseq1p1m1  10163  frec2uzsucd  10475  frec2uzrdg  10483  frecuzrdgsuc  10488  frecuzrdgg  10490  frecuzrdgsuctlem  10497  seqeq1  10524  seqeq2  10525  seqeq3  10526  seqvalcd  10535  seq3f1olemp  10589  hashprg  10882  shftdm  10969  resqrexlemfp1  11156  negfi  11374  sumeq1  11501  sumeq2  11505  zsumdc  11530  isumss2  11539  fsumsplitsnun  11565  isumclim3  11569  fisumcom2  11584  isumshft  11636  prodeq1f  11698  prodeq2w  11702  prodeq2  11703  zproddc  11725  fprodm1s  11747  fprodp1s  11748  fprodcom2fi  11772  fprodsplitf  11778  ege2le3  11817  efgt1p2  11841  dfphi2  12361  prmdiveq  12377  pceulem  12435  sloteq  12626  setsslid  12672  ressval2  12687  ecqusaddd  13311  ringidvalg  13460  zrhpropd  14125  metreslem  14559  comet  14678  cnmetdval  14708  dvmptfsum  14904  dvply1  14943  lgsdi  15194  lgseisenlem2  15228  lgsquadlem3  15236  redcwlpolemeq1  15614