MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr3g Structured version   Visualization version   GIF version

Theorem 3eqtr3g 2880
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
StepHypRef Expression
1 3eqtr3g.2 . . 3 𝐴 = 𝐶
2 3eqtr3g.1 . . 3 (𝜑𝐴 = 𝐵)
31, 2syl5eqr 2871 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr3g.3 . 2 𝐵 = 𝐷
53, 4syl6eq 2873 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538
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 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815
This theorem is referenced by:  csbnest1g  4353  disjdif2  4400  diftpsn3  4708  tppreqb  4711  xpid11  5779  cores2  6090  funcoeqres  6627  fvunsn  6923  caovmo  7370  dftpos2  7896  fvmpocurryd  7924  tfrlem16  8016  oev2  8135  domss2  8664  enp1ilem  8740  fipreima  8818  dfac5lem3  9540  fpwwe2lem13  10053  canthwelem  10061  canthp1lem2  10064  reclem3pr  10460  mulcmpblnrlem  10481  1idsr  10509  mulgt0sr  10516  mul02lem2  10806  ine0  11064  lo1eq  14916  rlimeq  14917  sumeq2ii  15041  fsumf1o  15071  sumss  15072  fsumss  15073  fsumadd  15087  fsumcom2  15120  fsum0diag2  15129  fsummulc2  15130  fsumrelem  15153  isumshft  15185  mertenslem1  15231  prodeq2ii  15258  fprodf1o  15291  prodss  15292  fprodss  15293  fprodmul  15305  fproddiv  15306  fprodcom2  15329  fprodmodd  15342  fprodefsum  15439  bitsinv1  15780  bitsinvp1  15787  4sqlem10  16272  setsnid  16530  topnpropd  16701  xpsff1o  16831  homfeqbas  16957  comfffval2  16962  comfeq  16967  oppchomfpropd  16987  isssc  17081  funcpropd  17161  hofpropd  17508  eqglact  18322  symgvalstruct  18516  lsmmod2  18793  vrgpinv  18886  frgpnabllem1  18984  frgpnabllem2  18985  gsum2dlem2  19082  dprddisj2  19152  ablfac1eulem  19185  ringpropd  19326  crngpropd  19327  mulgass3  19381  rngidpropd  19439  invrpropd  19442  isrhm2d  19474  subrgpropd  19561  rhmpropd  19562  lss0v  19779  lidlrsppropd  19994  ressmpladd  20695  ressmplmul  20696  ressmplvsca  20697  eqcoe1ply1eq  20924  resstopn  21789  lecldbas  21822  isref  22112  txhaus  22250  qustgplem  22724  tuslem  22871  imasdsf1olem  22978  metustsym  23160  reconnlem1  23429  voliunlem1  24152  ismbf3d  24256  i1fima  24280  i1fd  24283  itgfsum  24428  dvmptc  24559  dvmptfsum  24576  dvfsumle  24622  dvfsumlem2  24628  itgsubst  24650  atantayl2  25522  chtdif  25741  ppidif  25746  pythi  28631  hvsubeq0i  28844  hvaddcani  28846  cmcmlem  29372  pj11i  29492  hosubeq0i  29607  riesz3i  29843  pjclem1  29976  pjclem3  29978  st0  30030  chirredi  30175  mdsymi  30192  difeq  30287  unidifsnne  30303  1nei  30482  subrgchr  30897  locfinref  31163  esumpfinvallem  31407  esum2dlem  31425  carsgclctun  31653  ballotlemgun  31856  cvmliftmolem1  32602  cvmlift3lem6  32645  msubff1  32877  isfne  33761  isfne4  33762  isfne4b  33763  bj-1uplth  34404  bj-2uplth  34418  matunitlindflem1  35011  ptrest  35014  poimirlem3  35018  poimirlem4  35019  poimirlem8  35023  poimirlem15  35030  mblfinlem2  35053  voliunnfl  35059  cdlemg47  37990  ltrnco4  37993  sn-1ne2  39410  sn-inelr  39524  eldioph2  39633  binomcxplemdvbinom  40991  binomcxplemnotnn0  40994  compne  41079  rnfdmpr  43776
  Copyright terms: Public domain W3C validator