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

Theorem equcoms 1933
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 1930 . 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 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  equtr  1934  equeuclr  1936  equtr2OLD  1942  stdpc7  1944  equvinvOLD  1948  spfw  1951  spfwOLD  1952  cbvalw  1954  alcomiw  1957  ax8  1982  elequ1  1983  ax9  1989  elequ2  1990  19.8aOLD  2039  sbequ12r  2097  cbvalv1  2162  cbval  2258  cbvalv  2260  sbequ  2363  sb9  2413  reu8  3368  sbcco2  3425  opeliunxp  5083  elrnmpt1  5282  iotaval  5765  fvn0ssdmfun  6243  elabrex  6383  snnex  6839  tfisi  6927  tfinds2  6932  opabex3d  7014  opabex3  7015  mpt2curryd  7259  boxriin  7813  ixpiunwdom  8356  elirrv  8364  rabssnn0fi  12602  fproddivf  14503  prmodvdslcmf  15535  imasvscafn  15966  1mavmul  20115  ptbasfi  21136  elmptrab  21382  pcoass  22563  iundisj2  23041  dchrisumlema  24894  dchrisumlem2  24896  cusgrafilem2  25774  frgrancvvdeqlem9  26334  iundisj2f  28591  iundisj2fi  28749  bnj1014  30090  cvmsss2  30316  ax8dfeq  30754  bj-ssbid1ALT  31643  bj-cbvexw  31657  bj-sb  31670  finxpreclem6  32205  wl-nfs1t  32299  wl-equsb4  32313  wl-euequ1f  32331  wl-ax11-lem8  32344  matunitlindflem1  32371  poimirlem26  32401  mblfinlem2  32413  sdclem2  32504  axc11-o  33050  rexzrexnn0  36182  elabrexg  38025  disjinfi  38171  dvnmptdivc  38625  iblsplitf  38659  vonn0ioo2  39378  vonn0icc2  39380  cusgrfilem2  40667  frgrncvvdeq  41475  opeliun2xp  41899
  Copyright terms: Public domain W3C validator