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

Theorem equcoms 2028
 Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
equcoms.1 (𝑥 = 𝑦𝜑)
Assertion
Ref Expression
equcoms (𝑦 = 𝑥𝜑)

Proof of Theorem equcoms
StepHypRef Expression
1 equcomi 2025 . 2 (𝑦 = 𝑥𝑥 = 𝑦)
2 equcoms.1 . 2 (𝑥 = 𝑦𝜑)
31, 2syl 17 1 (𝑦 = 𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4 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 1971  ax-7 2016 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782 This theorem is referenced by:  equtr  2029  equeuclr  2031  spfw  2041  cbvalw  2043  alcomiw  2051  alcomiwOLD  2052  sbequOLD  2093  ax8  2121  elequ1  2122  ax9  2129  elequ2  2130  stdpc7  2254  sbequ12r  2256  sbequvvOLD  2337  cbvalv1  2363  cbval  2418  cbvalvOLD  2422  sb9  2563  sbequALT  2599  ax9ALT  2820  sbralie  3456  reu8  3710  sbcco2  3785  reu8nf  3844  sbcop1  5366  opeliunxp  5606  elrnmpt1  5817  elidinxp  5898  fvn0ssdmfun  6833  elabrex  6994  tfisi  7567  tfinds2  7572  opabex3d  7661  opabex3rd  7662  opabex3  7663  mpocurryd  7931  boxriin  8500  ixpiunwdom  9051  elirrv  9057  rabssnn0fi  13358  fproddivf  15341  prmodvdslcmf  16381  1mavmul  21157  ptbasfi  22189  elmptrab  22435  pcoass  23632  iundisj2  24156  dchrisumlema  26075  dchrisumlem2  26077  cusgrfilem2  27249  frgrncvvdeq  28097  frgr2wwlk1  28117  iundisj2f  30351  iundisj2fi  30531  bnj1014  32290  cvmsss2  32578  gonarlem  32698  ax8dfeq  33100  bj-ssbid1ALT  34055  bj-cbvexw  34066  bj-sb  34078  finxpreclem6  34758  ralssiun  34769  wl-nfs1t  34887  wl-equsb4  34903  wl-euequf  34920  wl-ax11-lem8  34934  matunitlindflem1  34998  poimirlem26  35028  mblfinlem2  35040  sdclem2  35125  axc11-o  36192  rexzrexnn0  39661  elabrexg  41595  disjinfi  41745  dvnmptdivc  42506  iblsplitf  42538  vonn0ioo2  43255  vonn0icc2  43257  funressnvmo  43563  ichcircshi  43897  ichreuopeq  43916  paireqne  43954  reuopreuprim  43969  uspgrsprf1  44301  opeliun2xp  44660
 Copyright terms: Public domain W3C validator