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

Theorem equcoms 1708
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 (𝑥 = 𝑦𝜑)
Assertion
Ref Expression
equcoms (𝑦 = 𝑥𝜑)

Proof of Theorem equcoms
StepHypRef Expression
1 equcomi 1704 . 2 (𝑦 = 𝑥𝑥 = 𝑦)
2 equcoms.1 . 2 (𝑥 = 𝑦𝜑)
31, 2syl 14 1 (𝑦 = 𝑥𝜑)
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 106  ax-gen 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  equtr  1709  equtr2  1711  equequ2  1713  ax10o  1715  cbvalv1  1751  cbvexv1  1752  cbvalh  1753  cbvexh  1755  equvini  1758  stdpc7  1770  sbequ12r  1772  sbequ12a  1773  sbequ  1840  sb6rf  1853  cbvalvw  1919  cbvexvw  1920  sb9v  1978  sb6a  1988  mo2n  2054  elequ1  2152  elequ2  2153  cleqh  2277  cbvab  2301  sbralie  2721  reu8  2933  sbcco2  2985  snnex  4447  tfisi  4585  opeliunxp  4680  elrnmpt1  4877  rnxpid  5062  iotaval  5188  elabrex  5756  opabex3d  6119  opabex3  6120  enq0ref  7429  fproddivapf  11632  setindis  14579  bdsetindis  14581
  Copyright terms: Public domain W3C validator