Theorem 3eqtr3g 2802

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731

This theorem is referenced by:  csbnest1g  4368  disjdif2  4418  diftpsn3  4740  tppreqb  4743  xpid11  5838  cores2  6160  funcoeqres  6742  fvunsn  7045  caovmo  7500  dftpos2  8043  fvmpocurryd  8071  tfrlem16  8208  oev2  8329  domss2  8888  enp1ilem  9012  fipreima  9086  dfac5lem3  9865  fpwwe2lem12  10382  canthwelem  10390  canthp1lem2  10393  reclem3pr  10789  mulcmpblnrlem  10810  1idsr  10838  mulgt0sr  10845  mul02lem2  11135  ine0  11393  lo1eq  15258  rlimeq  15259  sumeq2ii  15386  fsumf1o  15416  sumss  15417  fsumss  15418  fsumadd  15433  fsumcom2  15467  fsum0diag2  15476  fsummulc2  15477  fsumrelem  15500  isumshft  15532  mertenslem1  15577  prodeq2ii  15604  fprodf1o  15637  prodss  15638  fprodss  15639  fprodmul  15651  fproddiv  15652  fprodcom2  15675  fprodmodd  15688  fprodefsum  15785  bitsinv1  16130  bitsinvp1  16137  4sqlem10  16629  setsnid  16891  setsnidOLD  16892  topnpropd  17128  xpsff1o  17259  homfeqbas  17386  comfffval2  17391  comfeq  17396  oppchomfpropd  17418  isssc  17513  funcpropd  17597  hofpropd  17966  eqglact  18788  symgvalstruct  18985  symgvalstructOLD  18986  lsmmod2  19263  vrgpinv  19356  frgpnabllem1  19455  frgpnabllem2  19456  gsum2dlem2  19553  dprddisj2  19623  ablfac1eulem  19656  ringpropd  19802  crngpropd  19803  mulgass3  19860  rngidpropd  19918  invrpropd  19921  isrhm2d  19953  subrgpropd  20040  rhmpropd  20041  lss0v  20259  lidlrsppropd  20482  ressmpladd  21211  ressmplmul  21212  ressmplvsca  21213  eqcoe1ply1eq  21449  resstopn  22318  lecldbas  22351  isref  22641  txhaus  22779  qustgplem  23253  tuslem  23399  tuslemOLD  23400  imasdsf1olem  23507  metustsym  23692  reconnlem1  23970  voliunlem1  24695  ismbf3d  24799  i1fima  24823  i1fd  24826  itgfsum  24972  dvmptc  25103  dvmptfsum  25120  dvfsumle  25166  dvfsumlem2  25172  itgsubst  25194  atantayl2  26069  chtdif  26288  ppidif  26293  pythi  29191  hvsubeq0i  29404  hvaddcani  29406  cmcmlem  29932  pj11i  30052  hosubeq0i  30167  riesz3i  30403  pjclem1  30536  pjclem3  30538  st0  30590  chirredi  30735  mdsymi  30752  difeq  30844  unidifsnne  30863  1nei  31050  subrgchr  31470  locfinref  31770  esumpfinvallem  32021  esum2dlem  32039  carsgclctun  32267  ballotlemgun  32470  cvmliftmolem1  33222  cvmlift3lem6  33265  msubff1  33497  isfne  34507  isfne4  34508  isfne4b  34509  bj-1uplth  35176  bj-2uplth  35190  matunitlindflem1  35752  ptrest  35755  poimirlem3  35759  poimirlem4  35760  poimirlem8  35764  poimirlem15  35771  mblfinlem2  35794  voliunnfl  35800  cdlemg47  38729  ltrnco4  38732  sn-1ne2  40275  sn-0tie0  40401  sn-inelr  40415  eldioph2  40564  binomcxplemdvbinom  41924  binomcxplemnotnn0  41927  compne  42012  rnfdmpr  44724