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

Theorem equcoms 1735
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  |-  ( x  =  y  ->  ph )
Assertion
Ref Expression
equcoms  |-  ( y  =  x  ->  ph )

Proof of Theorem equcoms
StepHypRef Expression
1 equcomi 1733 . 2  |-  ( y  =  x  ->  x  =  y )
2 equcoms.1 . 2  |-  ( x  =  y  ->  ph )
31, 2syl 16 1  |-  ( y  =  x  ->  ph )
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 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730
This theorem depends on definitions:  df-bi 185  df-ex 1588
This theorem is referenced by:  equtr  1736  stdpc7  1741  equtr2  1742  ax13b  1745  spfw  1746  cbvalw  1748  alcomiw  1751  elequ1  1761  elequ2  1763  19.8a  1795  sbequ12r  1946  sbequ12aOLD  1948  cbval  1978  sbequ  2074  sb6rfOLD  2130  sb9  2133  sb6aOLD  2163  ax13fromc9  2213  axc11-o  2259  euequ1  2266  moOLD  2312  cleqhOLD  2567  cbvabOLD  2593  reu8  3255  sbcco2  3311  opeliunxp  4991  elrnmpt1  5189  iotaval  5493  elabrex  6062  snnex  6485  tfisi  6572  tfinds2  6577  opabex3d  6658  opabex3  6659  mpt2curryd  6891  boxriin  7408  ixpiunwdom  7910  elirrv  7916  imasvscafn  14586  1mavmul  18479  ptbasfi  19279  elmptrab  19525  pcoass  20721  iundisj2  21156  dchrisumlema  22863  dchrisumlem2  22865  cusgrafilem2  23533  iundisj2f  26076  iundisj2fi  26219  voliune  26782  volfiniune  26783  cvmsss2  27300  ax8dfeq  27749  wl-nfs1t  28508  wl-equsb4  28522  wl-ax11-lem8  28549  mblfinlem2  28570  sdclem2  28779  rexzrexnn0  29283  frgrancvvdeqlem9  30775  opeliun2xp  30861  rabssnn0fi  30888  bnj1014  32256  bj-cbvalv  32535  bj-cleqh  32596
  Copyright terms: Public domain W3C validator