Theorem 3eqtr4g 2289

Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3eqtr4g.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4g.2	⊢ 𝐶 = 𝐴
3eqtr4g.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3eqtr4g	⊢ (𝜑 → 𝐶 = 𝐷)

Proof of Theorem 3eqtr4g

Step	Hyp	Ref	Expression
1		3eqtr4g.2	. . 3 ⊢ 𝐶 = 𝐴
2		3eqtr4g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	eqtrid 2276	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2282	1 ⊢ (𝜑 → 𝐶 = 𝐷)

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  5638  fveq2  5639  fvres  5663  csbfv12g  5679  fnimapr  5706  fndmin  5754  fprg  5837  fsnunfv  5855  fsnunres  5856  fliftf  5940  isoini2  5960  riotaeqdv  5972  riotabidv  5973  riotauni  5978  riotabidva  5989  snriota  6003  oveq  6024  oveq1  6025  oveq2  6026  oprabbid  6074  mpoeq123  6080  mpoeq123dva  6082  mpoeq3dva  6085  resmpo  6119  ovres  6162  f1ocnvd  6225  ofeqd  6237  ofeq  6238  ofreq  6239  f1od2  6400  ovtposg  6425  recseq  6472  tfr2a  6487  rdgeq1  6537  rdgeq2  6538  freceq1  6558  freceq2  6559  eceq1  6737  eceq2  6739  qseq1  6752  qseq2  6753  uniqs  6762  ecinxp  6779  qsinxp  6780  erovlem  6796  ixpeq1  6878  supeq1  7185  supeq2  7188  supeq3  7189  supeq123d  7190  infeq1  7210  infeq2  7213  infeq3  7214  infeq123d  7215  infisoti  7231  djueq12  7238  acneq  7417  addpiord  7536  mulpiord  7537  00sr  7989  negeq  8372  csbnegg  8377  negsubdi  8435  mulneg1  8574  deceq1  9615  deceq2  9616  xnegeq  10062  fseq1p1m1  10329  frec2uzsucd  10664  frec2uzrdg  10672  frecuzrdgsuc  10677  frecuzrdgg  10679  frecuzrdgsuctlem  10686  seqeq1  10713  seqeq2  10714  seqeq3  10715  seqvalcd  10724  seq3f1olemp  10778  hashprg  11073  s1eq  11200  s1prc  11204  s2eqd  11355  s3eqd  11356  s4eqd  11357  s5eqd  11358  s6eqd  11359  s7eqd  11360  s8eqd  11361  shftdm  11400  resqrexlemfp1  11587  negfi  11806  sumeq1  11933  sumeq2  11937  zsumdc  11963  isumss2  11972  fsumsplitsnun  11998  isumclim3  12002  fisumcom2  12017  isumshft  12069  prodeq1f  12131  prodeq2w  12135  prodeq2  12136  zproddc  12158  fprodm1s  12180  fprodp1s  12181  fprodcom2fi  12205  fprodsplitf  12211  ege2le3  12250  efgt1p2  12274  dfphi2  12810  prmdiveq  12826  pceulem  12885  sloteq  13105  setsslid  13151  ressval2  13167  ecqusaddd  13843  ringidvalg  13993  zrhpropd  14659  metreslem  15123  comet  15242  cnmetdval  15272  dvmptfsum  15468  dvply1  15508  lgsdi  15785  lgseisenlem2  15819  lgsquadlem3  15827  uhgrvtxedgiedgb  16013  usgredg2v  16094  depindlem1  16376  redcwlpolemeq1  16710