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  4196  mpteq12f  4211  suceq  4547  xpeq1  4788  xpeq2  4789  csbxpg  4856  csbdmg  4975  rneq  5009  reseq1  5057  reseq2  5058  csbresg  5066  resindm  5105  resmpt  5111  resmptf  5113  imaeq1  5121  imaeq2  5122  mptcnv  5190  csbrng  5249  dmpropg  5260  rnpropg  5267  cores  5291  cores2  5300  xpcom  5334  iotaeq  5346  iotabi  5347  fntpg  5437  funimaexg  5465  fveq1  5694  fveq2  5695  fvres  5719  csbfv12g  5736  fnimapr  5763  fndmin  5816  fprg  5898  fsnunfv  5916  fsnunres  5917  fliftf  6005  isoini2  6025  riotaeqdv  6039  riotabidv  6040  riotauni  6045  riotabidva  6056  snriota  6070  oveq  6091  oveq1  6092  oveq2  6093  oprabbid  6141  mpoeq123  6147  mpoeq123dva  6149  mpoeq3dva  6152  resmpo  6186  ovres  6229  f1ocnvd  6292  ofeqd  6304  ofeq  6305  ofreq  6306  f1od2  6471  ovtposg  6530  recseq  6577  tfr2a  6592  rdgeq1  6642  rdgeq2  6643  freceq1  6663  freceq2  6664  eceq1  6842  eceq2  6844  qseq1  6857  qseq2  6858  uniqs  6867  ecinxp  6884  qsinxp  6885  erovlem  6901  ixpeq1  6991  supeq1  7326  supeq2  7329  supeq3  7330  supeq123d  7331  infeq1  7351  infeq2  7354  infeq3  7355  infeq123d  7356  infisoti  7372  djueq12  7379  acneq  7558  addpiord  7683  mulpiord  7684  00sr  8136  negeq  8519  csbnegg  8524  negsubdi  8582  mulneg1  8722  deceq1  9781  deceq2  9782  xnegeq  10229  fseq1p1m1  10501  frec2uzsucd  10838  frec2uzrdg  10846  frecuzrdgsuc  10851  frecuzrdgg  10853  frecuzrdgsuctlem  10860  seqeq1  10887  seqeq2  10888  seqeq3  10889  seqvalcd  10898  seq3f1olemp  10952  hashprg  11249  s1eq  11387  s1prc  11391  s2eqd  11542  s3eqd  11543  s4eqd  11544  s5eqd  11545  s6eqd  11546  s7eqd  11547  s8eqd  11548  shftdm  11587  resqrexlemfp1  11775  negfi  11994  sumeq1  12121  sumeq2  12125  zsumdc  12151  isumss2  12160  fsumsplitsnun  12186  isumclim3  12190  fisumcom2  12205  isumshft  12257  prodeq1f  12319  prodeq2w  12323  prodeq2  12324  zproddc  12346  fprodm1s  12368  fprodp1s  12369  fprodcom2fi  12393  fprodsplitf  12399  ege2le3  12438  efgt1p2  12462  dfphi2  12998  prmdiveq  13014  pceulem  13073  sloteq  13357  setsslid  13403  ressval2  13420  ecqusaddd  14041  gsumzfi  14158  gsumsubmclfi  14163  ringidvalg  14264  zrhpropd  14961  ressascl  15039  asclpropd  15040  metreslem  15481  comet  15600  cnmetdval  15630  dvmptfsum  15826  dvply1  15866  lgsdi  16156  lgseisenlem2  16190  lgsquadlem3  16198  uhgrvtxedgiedgb  16384  usgredg2v  16465  depindlem1  16747  redcwlpolemeq1  17104