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

Theorem equcoms 1693
Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
equcoms.1  |-  ( x  =  y  ->  ph )
Assertion
Ref Expression
equcoms  |-  ( y  =  x  ->  ph )

Proof of Theorem equcoms
StepHypRef Expression
1 equcomi 1691 . 2  |-  ( y  =  x  ->  x  =  y )
2 equcoms.1 . 2  |-  ( x  =  y  ->  ph )
31, 2syl 16 1  |-  ( y  =  x  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  equtr  1694  equtr2  1700  ax12b  1701  ax12bOLD  1702  spfw  1703  spwOLD  1707  cbvalw  1714  cbvalvwOLD  1716  alcomiw  1718  elequ1  1728  elequ2  1730  19.8a  1762  stdpc7  1942  sbequ12r  1945  sbequ12a  1946  a9e  1952  cbval  1982  ax12OLD  2020  ax10oOLD  2039  equvini  2079  equviniOLD  2080  sbequi  2136  sbequ  2138  sb6rf  2166  sb6a  2192  ax12from12o  2232  ax10o-o  2279  mo  2302  cleqh  2532  cbvab  2553  reu8  3122  sbcco2  3176  snnex  4705  tfisi  4830  tfinds2  4835  opeliunxp  4921  elrnmpt1  5111  iotaval  5421  elabrex  5977  opabex3d  5981  opabex3  5982  boxriin  7096  ixpiunwdom  7551  elirrv  7557  imasvscafn  13754  ptbasfi  17605  elmptrab  17851  pcoass  19041  iundisj2  19435  dchrisumlema  21174  dchrisumlem2  21176  cusgrafilem2  21481  iundisj2f  24022  iundisj2fi  24145  voliune  24577  volfiniune  24578  cvmsss2  24953  ax13dfeq  25418  mblfinlem  26234  sdclem2  26437  rexzrexnn0  26855  frgrancvvdeqlem9  28367  bnj1014  29268  ax10oNEW7  29413  cbvalwwAUX7  29456  equviniNEW7  29464  sbequNEW7  29517  sb6rfNEW7  29529  sb6aNEW7  29548  cbvalOLD7  29662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator