Theorem 3eqtr3g 2856

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 2847	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2849	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  csbnest1g  4337  disjdif2  4386  diftpsn3  4695  tppreqb  4698  xpid11  5766  cores2  6079  funcoeqres  6620  fvunsn  6918  caovmo  7365  dftpos2  7892  fvmpocurryd  7920  tfrlem16  8012  oev2  8131  domss2  8660  enp1ilem  8736  fipreima  8814  dfac5lem3  9536  fpwwe2lem13  10053  canthwelem  10061  canthp1lem2  10064  reclem3pr  10460  mulcmpblnrlem  10481  1idsr  10509  mulgt0sr  10516  mul02lem2  10806  ine0  11064  lo1eq  14917  rlimeq  14918  sumeq2ii  15042  fsumf1o  15072  sumss  15073  fsumss  15074  fsumadd  15088  fsumcom2  15121  fsum0diag2  15130  fsummulc2  15131  fsumrelem  15154  isumshft  15186  mertenslem1  15232  prodeq2ii  15259  fprodf1o  15292  prodss  15293  fprodss  15294  fprodmul  15306  fproddiv  15307  fprodcom2  15330  fprodmodd  15343  fprodefsum  15440  bitsinv1  15781  bitsinvp1  15788  4sqlem10  16273  setsnid  16531  topnpropd  16702  xpsff1o  16832  homfeqbas  16958  comfffval2  16963  comfeq  16968  oppchomfpropd  16988  isssc  17082  funcpropd  17162  hofpropd  17509  eqglact  18323  symgvalstruct  18517  lsmmod2  18794  vrgpinv  18887  frgpnabllem1  18986  frgpnabllem2  18987  gsum2dlem2  19084  dprddisj2  19154  ablfac1eulem  19187  ringpropd  19328  crngpropd  19329  mulgass3  19383  rngidpropd  19441  invrpropd  19444  isrhm2d  19476  subrgpropd  19563  rhmpropd  19564  lss0v  19781  lidlrsppropd  19996  ressmpladd  20697  ressmplmul  20698  ressmplvsca  20699  eqcoe1ply1eq  20926  resstopn  21791  lecldbas  21824  isref  22114  txhaus  22252  qustgplem  22726  tuslem  22873  imasdsf1olem  22980  metustsym  23162  reconnlem1  23431  voliunlem1  24154  ismbf3d  24258  i1fima  24282  i1fd  24285  itgfsum  24430  dvmptc  24561  dvmptfsum  24578  dvfsumle  24624  dvfsumlem2  24630  itgsubst  24652  atantayl2  25524  chtdif  25743  ppidif  25748  pythi  28633  hvsubeq0i  28846  hvaddcani  28848  cmcmlem  29374  pj11i  29494  hosubeq0i  29609  riesz3i  29845  pjclem1  29978  pjclem3  29980  st0  30032  chirredi  30177  mdsymi  30194  difeq  30289  unidifsnne  30308  1nei  30498  subrgchr  30916  locfinref  31194  esumpfinvallem  31443  esum2dlem  31461  carsgclctun  31689  ballotlemgun  31892  cvmliftmolem1  32641  cvmlift3lem6  32684  msubff1  32916  isfne  33800  isfne4  33801  isfne4b  33802  bj-1uplth  34443  bj-2uplth  34457  matunitlindflem1  35053  ptrest  35056  poimirlem3  35060  poimirlem4  35061  poimirlem8  35065  poimirlem15  35072  mblfinlem2  35095  voliunnfl  35101  cdlemg47  38032  ltrnco4  38035  sn-1ne2  39466  sn-0tie0  39576  sn-inelr  39590  eldioph2  39703  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  compne  41145  rnfdmpr  43837