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

Theorem equcoms 1641
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 1637 . 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 1383  ax-ie2 1428  ax-8 1440  ax-17 1464  ax-i9 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  equtr  1642  equtr2  1644  equequ2  1646  elequ1  1647  elequ2  1648  ax10o  1650  cbvalh  1683  cbvexh  1685  equvini  1688  stdpc7  1700  sbequ12r  1702  sbequ12a  1703  sbequ  1768  sb6rf  1781  sb9v  1902  sb6a  1912  mo2n  1976  cleqh  2187  cbvab  2210  reu8  2811  sbcco2  2862  snnex  4271  tfisi  4402  opeliunxp  4493  elrnmpt1  4686  rnxpid  4865  iotaval  4991  elabrex  5537  opabex3d  5892  opabex3  5893  enq0ref  6992  setindis  11862  bdsetindis  11864
  Copyright terms: Public domain W3C validator