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

Theorem equcoms 1944
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 1941 . 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 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702
This theorem is referenced by:  equtr  1945  equeuclr  1947  equtr2OLD  1953  stdpc7  1955  equvinvOLD  1959  spfw  1962  spfwOLD  1963  cbvalw  1965  alcomiw  1968  ax8  1993  elequ1  1994  ax9  2000  elequ2  2001  19.8aOLD  2050  sbequ12r  2109  cbvalv1  2174  cbval  2270  cbvalv  2272  sbequ  2375  sb9  2425  reu8  3389  sbcco2  3446  opeliunxp  5141  elrnmpt1  5344  fvn0ssdmfun  6316  elabrex  6466  snnexOLD  6931  tfisi  7020  tfinds2  7025  opabex3d  7106  opabex3  7107  mpt2curryd  7355  boxriin  7910  ixpiunwdom  8456  elirrv  8464  rabssnn0fi  12741  fproddivf  14662  prmodvdslcmf  15694  imasvscafn  16137  1mavmul  20294  ptbasfi  21324  elmptrab  21570  pcoass  22764  iundisj2  23257  dchrisumlema  25111  dchrisumlem2  25113  cusgrfilem2  26273  frgrncvvdeq  27072  iundisj2f  29289  iundisj2fi  29439  bnj1014  30791  cvmsss2  31017  ax8dfeq  31458  bj-ssbid1ALT  32343  bj-cbvexw  32359  bj-sb  32372  bj-cleljustab  32545  bj-ax9-2  32591  finxpreclem6  32904  wl-nfs1t  32995  wl-equsb4  33009  wl-euequ1f  33027  wl-ax11-lem8  33040  wl-ax8clv1  33049  wl-clelv2-just  33050  matunitlindflem1  33076  poimirlem26  33106  mblfinlem2  33118  sdclem2  33209  axc11-o  33755  rexzrexnn0  36887  elabrexg  38728  disjinfi  38889  dvnmptdivc  39490  iblsplitf  39523  vonn0ioo2  40241  vonn0icc2  40243  uspgrsprf1  41073  opeliun2xp  41429
  Copyright terms: Public domain W3C validator