ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  equcoms Unicode version

Theorem equcoms 1635
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 1633 . 2  |-  ( y  =  x  ->  x  =  y )
2 equcoms.1 . 2  |-  ( x  =  y  ->  ph )
31, 2syl 14 1  |-  ( y  =  x  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-8 1436  ax-17 1460  ax-i9 1464
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  equtr  1636  equtr2  1638  equequ2  1640  elequ1  1641  elequ2  1642  ax10o  1644  cbvalh  1677  cbvexh  1679  equvini  1682  stdpc7  1694  sbequ12r  1696  sbequ12a  1697  sbequ  1762  sb6rf  1775  sb9v  1896  sb6a  1906  mo2n  1970  cleqh  2179  cbvab  2202  reu8  2789  sbcco2  2838  snnex  4207  tfisi  4336  opeliunxp  4421  elrnmpt1  4613  rnxpid  4785  iotaval  4908  elabrex  5429  opabex3d  5779  opabex3  5780  enq0ref  6685  setindis  10920  bdsetindis  10922
  Copyright terms: Public domain W3C validator