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

Theorem equcoms 1681
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 1679 . 2  |-  ( y  =  x  ->  x  =  y )
2 equcoms.1 . 2  |-  ( x  =  y  ->  ph )
31, 2syl 15 1  |-  ( y  =  x  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  equtr  1682  equtr2  1688  ax12b  1689  ax12bOLD  1690  spfw  1691  spw  1694  cbvalw  1701  cbvalvw  1702  alcomiw  1704  elequ1  1713  elequ2  1715  19.8a  1747  stdpc7  1922  sbequ12r  1925  sbequ12a  1926  ax12olem1  1932  ax12  1940  ax10o  1957  cbval  1989  equvini  1992  sbequ  2065  sb6rf  2096  sb6a  2121  ax12from12o  2161  ax10o-o  2208  mo  2231  cleqh  2455  cbvab  2476  reu8  3037  tfinds2  4733  opabex3d  5852  boxriin  6943  elirrv  7398  elmptrab  17618  pcoass  18620  cvmsss2  24209  ax13dfeq  24713  sdclem2  25776  rexzrexnn0  26208  frgrancvvdeqlem9  27857  bnj1014  28737  ax10oNEW7  28882  cbvalwwAUX7  28923  equviniNEW7  28931  sbequNEW7  28983  sb6rfNEW7  28993  sb6aNEW7  29012  cbvalOLD7  29109
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675
This theorem depends on definitions:  df-bi 177  df-ex 1542
  Copyright terms: Public domain W3C validator