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

Theorem equcoms 1689
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 1687 . 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  1690  equtr2  1696  ax12b  1697  ax12bOLD  1698  spfw  1699  spwOLD  1703  cbvalw  1710  cbvalvwOLD  1712  alcomiw  1714  elequ1  1724  elequ2  1726  19.8a  1758  stdpc7  1938  sbequ12r  1941  sbequ12a  1942  a9e  1948  ax12OLD  1986  ax10oOLD  2005  cbval  2040  equvini  2043  equviniOLD  2044  sbequ  2113  sb6rf  2144  sb6a  2170  ax12from12o  2210  ax10o-o  2257  mo  2280  cleqh  2505  cbvab  2526  reu8  3094  sbcco2  3148  snnex  4676  tfisi  4801  tfinds2  4806  opeliunxp  4892  elrnmpt1  5082  iotaval  5392  elabrex  5948  opabex3d  5952  opabex3  5953  boxriin  7067  ixpiunwdom  7519  elirrv  7525  imasvscafn  13721  ptbasfi  17570  elmptrab  17816  pcoass  19006  iundisj2  19400  dchrisumlema  21139  dchrisumlem2  21141  cusgrafilem2  21446  iundisj2f  23987  iundisj2fi  24110  voliune  24542  volfiniune  24543  cvmsss2  24918  ax13dfeq  25373  mblfinlem  26147  sdclem2  26340  rexzrexnn0  26758  frgrancvvdeqlem9  28148  bnj1014  29041  ax10oNEW7  29186  cbvalwwAUX7  29227  equviniNEW7  29235  sbequNEW7  29287  sb6rfNEW7  29297  sb6aNEW7  29316  cbvalOLD7  29413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator