Theorem 3eqtr3g 2794

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

Syntax hints:   → wi 4   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  csbnest1g  4372  disjdif2  4420  diftpsn3  4747  tppreqb  4750  xpid11  5887  cores2  6224  funcoeqres  6811  fvunsn  7134  caovmo  7604  dftpos2  8193  fvmpocurryd  8221  tfrlem16  8332  oev2  8458  domss2  9074  enp1ilem  9188  fipreima  9268  dfac5lem3  10047  fpwwe2lem12  10565  canthwelem  10573  canthp1lem2  10576  reclem3pr  10972  mulcmpblnrlem  10993  1idsr  11021  mulgt0sr  11028  mul02lem2  11323  ine0  11585  lo1eq  15530  rlimeq  15531  sumeq2ii  15655  fsumf1o  15685  sumss  15686  fsumss  15687  fsumadd  15702  fsumcom2  15736  fsum0diag2  15745  fsummulc2  15746  fsumrelem  15770  isumshft  15804  mertenslem1  15849  prodeq2ii  15876  fprodf1o  15911  prodss  15912  fprodss  15913  fprodmul  15925  fproddiv  15926  fprodcom2  15949  fprodmodd  15962  fprodefsum  16060  bitsinv1  16411  bitsinvp1  16418  4sqlem10  16918  setsnid  17178  topnpropd  17399  xpsff1o  17531  homfeqbas  17662  comfffval2  17667  comfeq  17672  oppchomfpropd  17692  isssc  17787  funcpropd  17869  hofpropd  18233  eqglact  19154  symgvalstruct  19372  lsmmod2  19651  vrgpinv  19744  frgpnabllem1  19848  frgpnabllem2  19849  gsum2dlem2  19946  dprddisj2  20016  ablfac1eulem  20049  ringpropd  20269  crngpropd  20270  mulgass3  20333  rngidpropd  20395  invrpropd  20398  isrhm2d  20466  subrngpropd  20545  subrgpropd  20585  rhmpropd  20586  lss0v  21011  lidlrsppropd  21242  ressmpladd  22007  ressmplmul  22008  ressmplvsca  22009  eqcoe1ply1eq  22264  resstopn  23151  lecldbas  23184  isref  23474  txhaus  23612  qustgplem  24086  tuslem  24231  imasdsf1olem  24338  metustsym  24520  reconnlem1  24792  voliunlem1  25517  ismbf3d  25621  i1fima  25645  i1fd  25648  itgfsum  25794  dvmptc  25925  dvmptfsum  25942  dvfsumle  25988  dvfsumlem2  25994  itgsubst  26016  atantayl2  26902  chtdif  27121  ppidif  27126  fsumdvdsmul  27158  onleft  28252  oncutlt  28256  pythi  30921  hvsubeq0i  31134  hvaddcani  31136  cmcmlem  31662  pj11i  31782  hosubeq0i  31897  riesz3i  32133  pjclem1  32266  pjclem3  32268  st0  32320  chirredi  32465  mdsymi  32482  difeq  32588  unidifsnne  32606  1nei  32810  subrgchr  33298  ressply1evls1  33625  srapwov  33733  locfinref  33985  esumpfinvallem  34218  esum2dlem  34236  carsgclctun  34465  ballotlemgun  34669  cvmliftmolem1  35463  cvmlift3lem6  35506  msubff1  35738  isfne  36521  isfne4  36522  isfne4b  36523  bj-1uplth  37314  bj-2uplth  37328  matunitlindflem1  37937  ptrest  37940  poimirlem3  37944  poimirlem4  37945  poimirlem8  37949  poimirlem15  37956  mblfinlem2  37979  voliunnfl  37985  cdlemg47  41182  ltrnco4  41185  sn-1ne2  42703  sn-00idlem3  42832  sn-0tie0  42896  sn-inelr  42932  eldioph2  43194  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  compne  44867  rnfdmpr  47729  cycl3grtri  48423