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  4197  mpteq12f  4212  suceq  4549  xpeq1  4790  xpeq2  4791  csbxpg  4858  csbdmg  4977  rneq  5011  reseq1  5059  reseq2  5060  csbresg  5068  resindm  5108  resmpt  5114  resmptf  5116  imaeq1  5124  imaeq2  5125  mptcnv  5193  csbrng  5252  dmpropg  5263  rnpropg  5270  cores  5294  cores2  5303  xpcom  5337  iotaeq  5349  iotabi  5350  fntpg  5440  funimaexg  5468  fveq1  5697  fveq2  5698  fvres  5722  csbfv12g  5739  fnimapr  5766  fndmin  5819  fprg  5901  fsnunfv  5919  fsnunres  5920  fliftf  6008  isoini2  6028  riotaeqdv  6042  riotabidv  6043  riotauni  6048  riotabidva  6059  snriota  6073  oveq  6094  oveq1  6095  oveq2  6096  oprabbid  6144  mpoeq123  6150  mpoeq123dva  6152  mpoeq3dva  6155  resmpo  6189  ovres  6232  f1ocnvd  6295  ofeqd  6307  ofeq  6308  ofreq  6309  f1od2  6475  ovtposg  6534  recseq  6581  tfr2a  6596  rdgeq1  6646  rdgeq2  6647  freceq1  6667  freceq2  6668  eceq1  6846  eceq2  6848  qseq1  6861  qseq2  6862  uniqs  6871  ecinxp  6888  qsinxp  6889  erovlem  6905  ixpeq1  6995  supeq1  7332  supeq2  7335  supeq3  7336  supeq123d  7337  infeq1  7357  infeq2  7360  infeq3  7361  infeq123d  7362  infisoti  7378  djueq12  7385  acneq  7564  addpiord  7689  mulpiord  7690  00sr  8142  negeq  8526  csbnegg  8531  negsubdi  8589  mulneg1  8729  deceq1  9792  deceq2  9793  xnegeq  10246  fseq1p1m1  10518  frec2uzsucd  10859  frec2uzrdg  10867  frecuzrdgsuc  10872  frecuzrdgg  10874  frecuzrdgsuctlem  10881  seqeq1  10908  seqeq2  10909  seqeq3  10910  seqvalcd  10919  seq3f1olemp  10973  hashprg  11271  s1eq  11409  s1prc  11413  s2eqd  11564  s3eqd  11565  s4eqd  11566  s5eqd  11567  s6eqd  11568  s7eqd  11569  s8eqd  11570  shftdm  11609  resqrexlemfp1  11797  negfi  12017  sumeq1  12146  sumeq2  12150  zsumdc  12176  isumss2  12185  fsumsplitsnun  12211  isumclim3  12215  fisumcom2  12230  isumshft  12282  prodeq1f  12344  prodeq2w  12348  prodeq2  12349  zproddc  12371  fprodm1s  12393  fprodp1s  12394  fprodcom2fi  12418  fprodsplitf  12424  ege2le3  12463  efgt1p2  12487  dfphi2  13027  prmdiveq  13043  pceulem  13102  sloteq  13415  setsslid  13461  ressval2  13479  ecqusaddd  14100  gsumzfi  14248  gsumsubmclfi  14253  ringidvalg  14371  zrhpropd  15070  ressascl  15148  asclpropd  15149  metreslem  15606  comet  15725  cnmetdval  15755  dvmptfsum  15951  dvply1  15991  lgsdi  16361  lgseisenlem2  16395  lgsquadlem3  16403  uhgrvtxedgiedgb  16589  usgredg2v  16670  depindlem1  16952  redcwlpolemeq1  17311