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

Theorem equcoms 1667
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 1663 . 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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1408  ax-ie2 1453  ax-8 1465  ax-17 1489  ax-i9 1493
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  equtr  1668  equtr2  1670  equequ2  1672  elequ1  1673  elequ2  1674  ax10o  1676  cbvalh  1709  cbvexh  1711  equvini  1714  stdpc7  1726  sbequ12r  1728  sbequ12a  1729  sbequ  1794  sb6rf  1807  sb9v  1929  sb6a  1939  mo2n  2003  cleqh  2215  cbvab  2238  sbralie  2642  reu8  2851  sbcco2  2902  snnex  4337  tfisi  4469  opeliunxp  4562  elrnmpt1  4758  rnxpid  4941  iotaval  5067  elabrex  5625  opabex3d  5985  opabex3  5986  enq0ref  7205  setindis  12976  bdsetindis  12978
  Copyright terms: Public domain W3C validator