Theorem 3eqtr3g 2821

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  csbnest1g  4393  disjdif2  4439  diftpsn3  4765  tppreqb  4768  xpid11  5921  cores2  6274  funcoeqres  6879  fvunsn  7207  caovmo  7682  dftpos2  8288  fvmpocurryd  8316  tfrlem16  8429  oev2  8559  domss2  9183  enp1ilem  9297  fipreima  9375  dfac5lem3  10231  fpwwe2lem12  10754  canthwelem  10762  canthp1lem2  10765  reclem3pr  11161  mulcmpblnrlem  11182  1idsr  11210  mulgt0sr  11217  mul02lem2  11514  ine0  11778  lo1eq  15764  rlimeq  15765  sumeq2ii  15889  fsumf1o  15918  sumss  15919  fsumss  15920  fsumadd  15935  fsumcom2  15969  fsum0diag2  15978  fsummulc2  15979  fsumrelem  16003  isumshft  16037  mertenslem1  16082  prodeq2ii  16109  fprodf1o  16142  prodss  16143  fprodss  16144  fprodmul  16156  fproddiv  16157  fprodcom2  16180  fprodmodd  16193  fprodefsum  16290  bitsinv1  16641  bitsinvp1  16648  4sqlem10  17154  setsnid  17415  topnpropd  17636  xpsff1o  17768  homfeqbas  17899  comfffval2  17904  comfeq  17909  oppchomfpropd  17929  isssc  18024  funcpropd  18106  hofpropd  18470  eqglact  19420  symgvalstruct  19641  lsmmod2  19920  vrgpinv  20013  frgpnabllem1  20117  frgpnabllem2  20118  gsum2dlem2  20215  dprddisj2  20285  ablfac1eulem  20318  ringpropd  20549  crngpropd  20550  mulgass3  20613  rngidpropd  20675  invrpropd  20678  isrhm2d  20751  subrngpropd  20850  subrgpropd  20890  rhmpropd  20891  lss0v  21321  lidlrsppropd  21562  ressmpladd  22367  ressmplmul  22368  ressmplvsca  22369  eqcoe1ply1eq  22647  matunitlindflem1  23024  resstopn  23534  lecldbas  23567  isref  23858  txhaus  23996  qustgplem  24470  tuslem  24615  imasdsf1olem  24722  metustsym  24904  reconnlem1  25176  voliunlem1  25901  ismbf3d  26005  i1fima  26029  i1fd  26032  itgfsum  26177  dvmptc  26308  dvmptfsum  26325  dvfsumle  26371  dvfsumlem2  26377  itgsubst  26399  atantayl2  27296  chtdif  27515  ppidif  27520  fsumdvdsmul  27552  onleft  28676  oncutlt  28680  pythi  31482  hvsubeq0i  31695  hvaddcani  31697  cmcmlem  32223  pj11i  32343  hosubeq0i  32458  riesz3i  32694  pjclem1  32827  pjclem3  32829  st0  32881  chirredi  33026  mdsymi  33043  difeq  33186  unidifsnne  33204  1nei  33399  subrgchr  33867  ressply1evls1  34167  srapwov  34291  locfinref  34543  esumpfinvallem  34776  esum2dlem  34794  carsgclctun  35023  ballotlemgun  35227  cvmliftmolem1  36213  cvmlift3lem6  36256  msubff1  36488  isfne  37305  isfne4  37306  isfne4b  37307  bj-1uplth  38098  bj-2uplth  38112  ptrest  38729  poimirlem3  38733  poimirlem4  38734  poimirlem8  38738  poimirlem15  38745  mblfinlem2  38768  voliunnfl  38774  cdlemg47  41985  ltrnco4  41988  sn-1ne2  43523  sn-00idlem3  43644  sn-0tie0  43708  sn-inelr  43744  eldioph2  43966  binomcxplemdvbinom  45529  binomcxplemnotnn0  45532  compne  45615  rnfdmpr  48556  cycl3grtri  49250