Theorem 3eqtr3g 2667

Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.)

Hypotheses

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

Assertion

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

Proof of Theorem 3eqtr3g

Step	Hyp	Ref	Expression
1		3eqtr3g.2	. . 3 ⊢ 𝐴 = 𝐶
2		3eqtr3g.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	1, 2	syl5eqr 2658	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	syl6eq 2660	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  csbnest1g  3953  disjdif2  3999  diftpsn3  4273  tppreqb  4277  xpid11  5268  cores2  5565  funcoeqres  6080  fvunsn  6350  caovmo  6769  dftpos2  7256  fvmpt2curryd  7284  tfrlem16  7376  oev2  7490  domss2  8004  enp1ilem  8079  fipreima  8155  dfac5lem3  8831  fpwwe2lem13  9343  canthwelem  9351  canthp1lem2  9354  reclem3pr  9750  mulcmpblnrlem  9770  1idsr  9798  mulgt0sr  9805  mul02lem2  10092  ine0  10344  s1nzOLD  13240  lo1eq  14147  rlimeq  14148  sumeq2ii  14271  fsumf1o  14301  sumss  14302  fsumss  14303  fsumadd  14317  fsumcom2  14347  fsumcom2OLD  14348  fsum0diag2  14357  fsummulc2  14358  fsumrelem  14380  isumshft  14410  mertenslem1  14455  prodeq2ii  14482  fprodf1o  14515  prodss  14516  fprodss  14517  fprodmul  14529  fproddiv  14530  fprodcom2  14553  fprodcom2OLD  14554  fprodmodd  14567  fprodefsum  14664  bitsinv1  15002  bitsinvp1  15009  4sqlem10  15489  setsnid  15743  topnpropd  15920  xpsff1o  16051  homfeqbas  16179  comfffval2  16184  comfeq  16189  oppchomfpropd  16209  isssc  16303  funcpropd  16383  hofpropd  16730  eqglact  17468  lsmmod2  17912  vrgpinv  18005  frgpnabllem1  18099  frgpnabllem2  18100  gsum2dlem2  18193  dprddisj2  18261  ablfac1eulem  18294  ringpropd  18405  crngpropd  18406  mulgass3  18460  rngidpropd  18518  invrpropd  18521  isrhm2d  18551  subrgpropd  18637  rhmpropd  18638  lss0v  18837  lidlrsppropd  19051  ressmpladd  19278  ressmplmul  19279  ressmplvsca  19280  eqcoe1ply1eq  19488  resstopn  20800  lecldbas  20833  isref  21122  txhaus  21260  qustgplem  21734  tuslem  21881  imasdsf1olem  21988  metustsym  22170  reconnlem1  22437  voliunlem1  23125  ismbf3d  23227  i1fima  23251  i1fd  23254  itgfsum  23399  dvmptc  23527  dvmptfsum  23542  dvfsumle  23588  dvfsumlem2  23594  itgsubst  23616  atantayl2  24465  chtdif  24684  ppidif  24689  pythi  27089  hvsubeq0i  27304  hvaddcani  27306  cmcmlem  27834  pj11i  27954  hosubeq0i  28069  riesz3i  28305  pjclem1  28438  pjclem3  28440  st0  28492  chirredi  28637  mdsymi  28654  difeq  28739  subrgchr  29125  locfinref  29236  esumpfinvallem  29463  esum2dlem  29481  carsgclctun  29710  ballotlemgun  29913  cvmliftmolem1  30517  cvmlift3lem6  30560  msubff1  30707  isfne  31504  isfne4  31505  isfne4b  31506  bj-1uplth  32188  bj-2uplth  32202  matunitlindflem1  32575  ptrest  32578  poimirlem3  32582  poimirlem4  32583  poimirlem8  32587  poimirlem15  32594  mblfinlem2  32617  voliunnfl  32623  cdlemg47  35042  ltrnco4  35045  eldioph2  36343  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  rnfdmpr  40325