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  6535  recseq  6582  tfr2a  6597  rdgeq1  6647  rdgeq2  6648  freceq1  6668  freceq2  6669  eceq1  6847  eceq2  6849  qseq1  6862  qseq2  6863  uniqs  6872  ecinxp  6889  qsinxp  6890  erovlem  6906  ixpeq1  6997  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  9791  deceq2  9792  xnegeq  10245  fseq1p1m1  10517  frec2uzsucd  10858  frec2uzrdg  10866  frecuzrdgsuc  10871  frecuzrdgg  10873  frecuzrdgsuctlem  10880  seqeq1  10907  seqeq2  10908  seqeq3  10909  seqvalcd  10918  seq3f1olemp  10972  hashprg  11270  s1eq  11408  s1prc  11412  s2eqd  11563  s3eqd  11564  s4eqd  11565  s5eqd  11566  s6eqd  11567  s7eqd  11568  s8eqd  11569  shftdm  11608  resqrexlemfp1  11796  negfi  12016  sumeq1  12145  sumeq2  12149  zsumdc  12175  isumss2  12184  fsumsplitsnun  12210  isumclim3  12214  fisumcom2  12229  isumshft  12281  prodeq1f  12343  prodeq2w  12347  prodeq2  12348  zproddc  12370  fprodm1s  12392  fprodp1s  12393  fprodcom2fi  12417  fprodsplitf  12423  ege2le3  12462  efgt1p2  12486  dfphi2  13026  prmdiveq  13042  pceulem  13101  sloteq  13414  setsslid  13460  ressval2  13478  ecqusaddd  14099  gsumzfi  14247  gsumsubmclfi  14252  ringidvalg  14370  zrhpropd  15069  ressascl  15147  asclpropd  15148  metreslem  15623  comet  15742  cnmetdval  15772  dvmptfsum  15968  dvply1  16008  lgsdi  16378  lgseisenlem2  16412  lgsquadlem3  16420  uhgrvtxedgiedgb  16606  usgredg2v  16687  depindlem1  16969  redcwlpolemeq1  17328