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  5836  fsnunfv  5854  fsnunres  5855  fliftf  5939  isoini2  5959  riotaeqdv  5971  riotabidv  5972  riotauni  5977  riotabidva  5988  snriota  6002  oveq  6023  oveq1  6024  oveq2  6025  oprabbid  6073  mpoeq123  6079  mpoeq123dva  6081  mpoeq3dva  6084  resmpo  6118  ovres  6161  f1ocnvd  6224  ofeqd  6236  ofeq  6237  ofreq  6238  f1od2  6399  ovtposg  6424  recseq  6471  tfr2a  6486  rdgeq1  6536  rdgeq2  6537  freceq1  6557  freceq2  6558  eceq1  6736  eceq2  6738  qseq1  6751  qseq2  6752  uniqs  6761  ecinxp  6778  qsinxp  6779  erovlem  6795  ixpeq1  6877  supeq1  7184  supeq2  7187  supeq3  7188  supeq123d  7189  infeq1  7209  infeq2  7212  infeq3  7213  infeq123d  7214  infisoti  7230  djueq12  7237  acneq  7416  addpiord  7535  mulpiord  7536  00sr  7988  negeq  8371  csbnegg  8376  negsubdi  8434  mulneg1  8573  deceq1  9614  deceq2  9615  xnegeq  10061  fseq1p1m1  10328  frec2uzsucd  10662  frec2uzrdg  10670  frecuzrdgsuc  10675  frecuzrdgg  10677  frecuzrdgsuctlem  10684  seqeq1  10711  seqeq2  10712  seqeq3  10713  seqvalcd  10722  seq3f1olemp  10776  hashprg  11071  s1eq  11195  s1prc  11199  s2eqd  11350  s3eqd  11351  s4eqd  11352  s5eqd  11353  s6eqd  11354  s7eqd  11355  s8eqd  11356  shftdm  11382  resqrexlemfp1  11569  negfi  11788  sumeq1  11915  sumeq2  11919  zsumdc  11944  isumss2  11953  fsumsplitsnun  11979  isumclim3  11983  fisumcom2  11998  isumshft  12050  prodeq1f  12112  prodeq2w  12116  prodeq2  12117  zproddc  12139  fprodm1s  12161  fprodp1s  12162  fprodcom2fi  12186  fprodsplitf  12192  ege2le3  12231  efgt1p2  12255  dfphi2  12791  prmdiveq  12807  pceulem  12866  sloteq  13086  setsslid  13132  ressval2  13148  ecqusaddd  13824  ringidvalg  13973  zrhpropd  14639  metreslem  15103  comet  15222  cnmetdval  15252  dvmptfsum  15448  dvply1  15488  lgsdi  15765  lgseisenlem2  15799  lgsquadlem3  15807  uhgrvtxedgiedgb  15993  usgredg2v  16074  redcwlpolemeq1  16658