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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is used by:  csbnest1g  4397  disjdif2  4441  diftpsn3  4770  tppreqb  4773  xpid11  5922  cores2  6261  funcoeqres  6852  fvunsn  7177  caovmo  7647  dftpos2  8235  fvmpocurryd  8263  tfrlem16  8376  oev2  8504  domss2  9120  enp1ilem  9234  fipreima  9311  dfac5lem3  10114  fpwwe2lem12  10631  canthwelem  10639  canthp1lem2  10642  reclem3pr  11038  mulcmpblnrlem  11059  1idsr  11087  mulgt0sr  11094  mul02lem2  11391  ine0  11653  lo1eq  15624  rlimeq  15625  sumeq2ii  15749  fsumf1o  15779  sumss  15780  fsumss  15781  fsumadd  15796  fsumcom2  15830  fsum0diag2  15839  fsummulc2  15840  fsumrelem  15864  isumshft  15898  mertenslem1  15943  prodeq2ii  15970  fprodf1o  16005  prodss  16006  fprodss  16007  fprodmul  16019  fproddiv  16020  fprodcom2  16043  fprodmodd  16056  fprodefsum  16153  bitsinv1  16504  bitsinvp1  16511  4sqlem10  17011  setsnid  17272  topnpropd  17493  xpsff1o  17625  homfeqbas  17756  comfffval2  17761  comfeq  17766  oppchomfpropd  17786  isssc  17881  funcpropd  17963  hofpropd  18327  eqglact  19251  symgvalstruct  19471  lsmmod2  19750  vrgpinv  19843  frgpnabllem1  19947  frgpnabllem2  19948  gsum2dlem2  20045  dprddisj2  20115  ablfac1eulem  20148  ringpropd  20376  crngpropd  20377  mulgass3  20440  rngidpropd  20502  invrpropd  20505  isrhm2d  20578  subrngpropd  20676  subrgpropd  20716  rhmpropd  20717  lss0v  21146  lidlrsppropd  21387  ressmpladd  22188  ressmplmul  22189  ressmplvsca  22190  eqcoe1ply1eq  22468  resstopn  23352  lecldbas  23385  isref  23675  txhaus  23813  qustgplem  24287  tuslem  24432  imasdsf1olem  24539  metustsym  24721  reconnlem1  24993  voliunlem1  25718  ismbf3d  25822  i1fima  25846  i1fd  25849  itgfsum  25995  dvmptc  26126  dvmptfsum  26143  dvfsumle  26189  dvfsumlem2  26195  itgsubst  26217  atantayl2  27112  chtdif  27331  ppidif  27336  fsumdvdsmul  27368  onleft  28462  oncutlt  28466  pythi  31211  hvsubeq0i  31424  hvaddcani  31426  cmcmlem  31952  pj11i  32072  hosubeq0i  32187  riesz3i  32423  pjclem1  32556  pjclem3  32558  st0  32610  chirredi  32755  mdsymi  32772  difeq  32873  unidifsnne  32891  1nei  33091  subrgchr  33565  ressply1evls1  33864  srapwov  33988  locfinref  34240  esumpfinvallem  34473  esum2dlem  34491  carsgclctun  34720  ballotlemgun  34924  cvmliftmolem1  35781  cvmlift3lem6  35824  msubff1  36056  isfne  36878  isfne4  36879  isfne4b  36880  bj-1uplth  37671  bj-2uplth  37685  matunitlindflem1  38295  ptrest  38298  poimirlem3  38302  poimirlem4  38303  poimirlem8  38307  poimirlem15  38314  mblfinlem2  38337  voliunnfl  38343  cdlemg47  41538  ltrnco4  41541  sn-1ne2  43060  sn-00idlem3  43189  sn-0tie0  43253  sn-inelr  43289  eldioph2  43521  binomcxplemdvbinom  45091  binomcxplemnotnn0  45094  compne  45178  rnfdmpr  48046  cycl3grtri  48740