Theorem 3eqtr3g 2818

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 2809	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr3g.3	. 2 ⊢ 𝐵 = 𝐷
5	3, 4	eqtrdi 2811	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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  csbnest1g  4390  disjdif2  4436  diftpsn3  4765  tppreqb  4768  xpid11  5918  cores2  6258  funcoeqres  6852  fvunsn  7180  caovmo  7654  dftpos2  8246  fvmpocurryd  8274  tfrlem16  8387  oev2  8517  domss2  9141  enp1ilem  9255  fipreima  9332  dfac5lem3  10153  fpwwe2lem12  10676  canthwelem  10684  canthp1lem2  10687  reclem3pr  11083  mulcmpblnrlem  11104  1idsr  11132  mulgt0sr  11139  mul02lem2  11436  ine0  11698  lo1eq  15680  rlimeq  15681  sumeq2ii  15805  fsumf1o  15834  sumss  15835  fsumss  15836  fsumadd  15851  fsumcom2  15885  fsum0diag2  15894  fsummulc2  15895  fsumrelem  15919  isumshft  15953  mertenslem1  15998  prodeq2ii  16025  fprodf1o  16058  prodss  16059  fprodss  16060  fprodmul  16072  fproddiv  16073  fprodcom2  16096  fprodmodd  16109  fprodefsum  16206  bitsinv1  16557  bitsinvp1  16564  4sqlem10  17064  setsnid  17325  topnpropd  17546  xpsff1o  17678  homfeqbas  17809  comfffval2  17814  comfeq  17819  oppchomfpropd  17839  isssc  17934  funcpropd  18016  hofpropd  18380  eqglact  19330  symgvalstruct  19550  lsmmod2  19829  vrgpinv  19922  frgpnabllem1  20026  frgpnabllem2  20027  gsum2dlem2  20124  dprddisj2  20194  ablfac1eulem  20227  ringpropd  20458  crngpropd  20459  mulgass3  20522  rngidpropd  20584  invrpropd  20587  isrhm2d  20660  subrngpropd  20759  subrgpropd  20799  rhmpropd  20800  lss0v  21230  lidlrsppropd  21471  ressmpladd  22276  ressmplmul  22277  ressmplvsca  22278  eqcoe1ply1eq  22556  matunitlindflem1  22933  resstopn  23443  lecldbas  23476  isref  23767  txhaus  23905  qustgplem  24379  tuslem  24524  imasdsf1olem  24631  metustsym  24813  reconnlem1  25085  voliunlem1  25810  ismbf3d  25914  i1fima  25938  i1fd  25941  itgfsum  26086  dvmptc  26217  dvmptfsum  26234  dvfsumle  26280  dvfsumlem2  26286  itgsubst  26308  atantayl2  27207  chtdif  27426  ppidif  27431  fsumdvdsmul  27463  onleft  28557  oncutlt  28561  pythi  31363  hvsubeq0i  31576  hvaddcani  31578  cmcmlem  32104  pj11i  32224  hosubeq0i  32339  riesz3i  32575  pjclem1  32708  pjclem3  32710  st0  32762  chirredi  32907  mdsymi  32924  difeq  33025  unidifsnne  33043  1nei  33240  subrgchr  33708  ressply1evls1  34008  srapwov  34132  locfinref  34384  esumpfinvallem  34617  esum2dlem  34635  carsgclctun  34865  ballotlemgun  35069  cvmliftmolem1  35943  cvmlift3lem6  35986  msubff1  36218  isfne  37025  isfne4  37026  isfne4b  37027  bj-1uplth  37818  bj-2uplth  37832  ptrest  38433  poimirlem3  38437  poimirlem4  38438  poimirlem8  38442  poimirlem15  38449  mblfinlem2  38472  voliunnfl  38478  cdlemg47  41674  ltrnco4  41677  sn-1ne2  43211  sn-00idlem3  43340  sn-0tie0  43404  sn-inelr  43440  eldioph2  43672  binomcxplemdvbinom  45242  binomcxplemnotnn0  45245  compne  45329  rnfdmpr  48234  cycl3grtri  48928