Theorem 3eqtr4g 2290

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 2277	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4g.3	. 2 ⊢ 𝐷 = 𝐵
5	3, 4	eqtr4di 2283	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  rabbidva2  2797  rabeqf  2803  csbeq1  3141  csbeq2  3162  csbeq2d  3163  csbnestgf  3191  difeq1  3330  difeq2  3331  uneq2  3367  ineq2  3416  dfrab3ss  3499  ifeq1  3625  ifeq2  3626  ifbi  3643  pweq  3672  sneq  3700  csbsng  3750  rabsn  3756  preq1  3768  preq2  3769  tpeq1  3777  tpeq2  3778  tpeq3  3779  prprc1  3800  opeq1  3883  opeq2  3884  oteq1  3892  oteq2  3893  oteq3  3894  csbunig  3922  unieq  3923  inteq  3952  iineq1  4005  iineq2  4008  dfiin2g  4024  iinrabm  4054  iinin1m  4061  iinxprg  4066  opabbid  4175  mpteq12f  4190  suceq  4523  xpeq1  4763  xpeq2  4764  csbxpg  4831  csbdmg  4950  rneq  4984  reseq1  5032  reseq2  5033  csbresg  5041  resindm  5080  resmpt  5086  resmptf  5088  imaeq1  5096  imaeq2  5097  mptcnv  5165  csbrng  5224  dmpropg  5235  rnpropg  5242  cores  5266  cores2  5275  xpcom  5309  iotaeq  5321  iotabi  5322  fntpg  5412  funimaexg  5440  fveq1  5669  fveq2  5670  fvres  5694  csbfv12g  5710  fnimapr  5737  fndmin  5785  fprg  5867  fsnunfv  5885  fsnunres  5886  fliftf  5972  isoini2  5992  riotaeqdv  6004  riotabidv  6005  riotauni  6010  riotabidva  6021  snriota  6035  oveq  6056  oveq1  6057  oveq2  6058  oprabbid  6106  mpoeq123  6112  mpoeq123dva  6114  mpoeq3dva  6117  resmpo  6151  ovres  6194  f1ocnvd  6257  ofeqd  6268  ofeq  6269  ofreq  6270  f1od2  6431  ovtposg  6490  recseq  6537  tfr2a  6552  rdgeq1  6602  rdgeq2  6603  freceq1  6623  freceq2  6624  eceq1  6802  eceq2  6804  qseq1  6817  qseq2  6818  uniqs  6827  ecinxp  6844  qsinxp  6845  erovlem  6861  ixpeq1  6944  supeq1  7277  supeq2  7280  supeq3  7281  supeq123d  7282  infeq1  7302  infeq2  7305  infeq3  7306  infeq123d  7307  infisoti  7323  djueq12  7330  acneq  7509  addpiord  7631  mulpiord  7632  00sr  8084  negeq  8466  csbnegg  8471  negsubdi  8529  mulneg1  8668  deceq1  9713  deceq2  9714  xnegeq  10160  fseq1p1m1  10428  frec2uzsucd  10763  frec2uzrdg  10771  frecuzrdgsuc  10776  frecuzrdgg  10778  frecuzrdgsuctlem  10785  seqeq1  10812  seqeq2  10813  seqeq3  10814  seqvalcd  10823  seq3f1olemp  10877  hashprg  11173  s1eq  11305  s1prc  11309  s2eqd  11460  s3eqd  11461  s4eqd  11462  s5eqd  11463  s6eqd  11464  s7eqd  11465  s8eqd  11466  shftdm  11505  resqrexlemfp1  11692  negfi  11911  sumeq1  12038  sumeq2  12042  zsumdc  12068  isumss2  12077  fsumsplitsnun  12103  isumclim3  12107  fisumcom2  12122  isumshft  12174  prodeq1f  12236  prodeq2w  12240  prodeq2  12241  zproddc  12263  fprodm1s  12285  fprodp1s  12286  fprodcom2fi  12310  fprodsplitf  12316  ege2le3  12355  efgt1p2  12379  dfphi2  12915  prmdiveq  12931  pceulem  12990  sloteq  13215  setsslid  13261  ressval2  13277  ecqusaddd  13953  ringidvalg  14103  zrhpropd  14772  metreslem  15243  comet  15362  cnmetdval  15392  dvmptfsum  15588  dvply1  15628  lgsdi  15908  lgseisenlem2  15942  lgsquadlem3  15950  uhgrvtxedgiedgb  16136  usgredg2v  16217  depindlem1  16499  redcwlpolemeq1  16837  gfsumz  16867