Theorem 3eqtr4g 2289

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

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  rabbidva2  2786  rabeqf  2792  csbeq1  3130  csbeq2  3151  csbeq2d  3152  csbnestgf  3180  difeq1  3318  difeq2  3319  uneq2  3355  ineq2  3402  dfrab3ss  3485  ifeq1  3608  ifeq2  3609  ifbi  3626  pweq  3655  sneq  3680  csbsng  3730  rabsn  3736  preq1  3748  preq2  3749  tpeq1  3757  tpeq2  3758  tpeq3  3759  prprc1  3780  opeq1  3862  opeq2  3863  oteq1  3871  oteq2  3872  oteq3  3873  csbunig  3901  unieq  3902  inteq  3931  iineq1  3984  iineq2  3987  dfiin2g  4003  iinrabm  4033  iinin1m  4040  iinxprg  4045  opabbid  4154  mpteq12f  4169  suceq  4499  xpeq1  4739  xpeq2  4740  csbxpg  4807  csbdmg  4925  rneq  4959  reseq1  5007  reseq2  5008  csbresg  5016  resindm  5055  resmpt  5061  resmptf  5063  imaeq1  5071  imaeq2  5072  mptcnv  5139  csbrng  5198  dmpropg  5209  rnpropg  5216  cores  5240  cores2  5249  xpcom  5283  iotaeq  5295  iotabi  5296  fntpg  5386  funimaexg  5414  fveq1  5639  fveq2  5640  fvres  5664  csbfv12g  5680  fnimapr  5707  fndmin  5755  fprg  5838  fsnunfv  5856  fsnunres  5857  fliftf  5943  isoini2  5963  riotaeqdv  5975  riotabidv  5976  riotauni  5981  riotabidva  5992  snriota  6006  oveq  6027  oveq1  6028  oveq2  6029  oprabbid  6077  mpoeq123  6083  mpoeq123dva  6085  mpoeq3dva  6088  resmpo  6122  ovres  6165  f1ocnvd  6228  ofeqd  6240  ofeq  6241  ofreq  6242  f1od2  6403  ovtposg  6428  recseq  6475  tfr2a  6490  rdgeq1  6540  rdgeq2  6541  freceq1  6561  freceq2  6562  eceq1  6740  eceq2  6742  qseq1  6755  qseq2  6756  uniqs  6765  ecinxp  6782  qsinxp  6783  erovlem  6799  ixpeq1  6881  supeq1  7188  supeq2  7191  supeq3  7192  supeq123d  7193  infeq1  7213  infeq2  7216  infeq3  7217  infeq123d  7218  infisoti  7234  djueq12  7241  acneq  7420  addpiord  7539  mulpiord  7540  00sr  7992  negeq  8375  csbnegg  8380  negsubdi  8438  mulneg1  8577  deceq1  9618  deceq2  9619  xnegeq  10065  fseq1p1m1  10332  frec2uzsucd  10667  frec2uzrdg  10675  frecuzrdgsuc  10680  frecuzrdgg  10682  frecuzrdgsuctlem  10689  seqeq1  10716  seqeq2  10717  seqeq3  10718  seqvalcd  10727  seq3f1olemp  10781  hashprg  11076  s1eq  11203  s1prc  11207  s2eqd  11358  s3eqd  11359  s4eqd  11360  s5eqd  11361  s6eqd  11362  s7eqd  11363  s8eqd  11364  shftdm  11403  resqrexlemfp1  11590  negfi  11809  sumeq1  11936  sumeq2  11940  zsumdc  11966  isumss2  11975  fsumsplitsnun  12001  isumclim3  12005  fisumcom2  12020  isumshft  12072  prodeq1f  12134  prodeq2w  12138  prodeq2  12139  zproddc  12161  fprodm1s  12183  fprodp1s  12184  fprodcom2fi  12208  fprodsplitf  12214  ege2le3  12253  efgt1p2  12277  dfphi2  12813  prmdiveq  12829  pceulem  12888  sloteq  13108  setsslid  13154  ressval2  13170  ecqusaddd  13846  ringidvalg  13996  zrhpropd  14662  metreslem  15131  comet  15250  cnmetdval  15280  dvmptfsum  15476  dvply1  15516  lgsdi  15793  lgseisenlem2  15827  lgsquadlem3  15835  uhgrvtxedgiedgb  16021  usgredg2v  16102  depindlem1  16384  redcwlpolemeq1  16718