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

Theorem equcoms 1825
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 1822 . 2  |-  ( y  =  x  ->  x  =  y )
2 equcoms.1 . 2  |-  ( x  =  y  ->  ph )
31, 2syl 17 1  |-  ( y  =  x  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  equtr  1826  equtr2  1828  equequ2  1830  elequ1  1831  elequ2  1832  ax12b  1834  ax10o  1835  cbval  1877  equvini  1880  ax12  1882  stdpc7  1892  sbequ12r  1894  sbequ12a  1895  sbequ  1953  sb6rf  1986  sb6a  2079  mo  2138  cleqh  2353  cbvab  2374  reu8  2914  tfinds2  4591  boxriin  6791  elirrv  7244  elmptrab  17449  pcoass  18449  cvmsss2  23142  ax13dfeq  23489  dominc  24612  rninc  24613  pdiveql  25500  sdclem2  25784  rexzrexnn0  26217  bnj1014  28004
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-8 1623  ax-17 1628  ax-9 1684  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator