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

Theorem equcoms 1897
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 1894 . 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 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  equtr  1898  equeuclr  1900  equtr2OLD  1906  stdpc7  1908  equvinvOLD  1912  spfw  1915  cbvalw  1917  alcomiw  1920  ax8  1944  elequ1  1945  ax9  1951  elequ2  1952  19.8aOLD  1989  cbvalv1  2115  sbequ12r  2131  cbval  2162  cbvalv  2164  sbequ  2268  sb9  2318  reu8  3273  sbcco2  3330  opeliunxp  4987  elrnmpt1  5186  iotaval  5664  fvn0ssdmfun  6141  elabrex  6281  snnex  6737  tfisi  6825  tfinds2  6830  opabex3d  6911  opabex3  6912  mpt2curryd  7156  boxriin  7711  ixpiunwdom  8254  elirrv  8262  rabssnn0fi  12514  fproddivf  14424  prmodvdslcmf  15471  imasvscafn  15910  1mavmul  20074  ptbasfi  21095  elmptrab  21341  pcoass  22556  iundisj2  23000  dchrisumlema  24867  dchrisumlem2  24869  cusgrafilem2  25747  frgrancvvdeqlem9  26307  iundisj2f  28574  iundisj2fi  28739  bnj1014  30130  cvmsss2  30356  ax8dfeq  30791  bj-ssbid1ALT  31672  bj-cbvexw  31686  bj-sb  31699  finxpreclem6  32241  wl-nfs1t  32378  wl-equsb4  32392  wl-euequ1f  32410  wl-ax11-lem8  32423  matunitlindflem1  32450  poimirlem26  32480  mblfinlem2  32492  sdclem2  32583  axc11-o  33129  rexzrexnn0  36261  elabrexg  38111  disjinfi  38259  dvnmptdivc  38718  iblsplitf  38752  vonn0ioo2  39475  vonn0icc2  39477  cusgrfilem2  40764  frgrncvvdeq  41572  opeliun2xp  41996
  Copyright terms: Public domain W3C validator