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

Theorem equcoms 1638
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 1635 . 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-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1381  ax-ie2 1426  ax-8 1438  ax-17 1462  ax-i9 1466
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  equtr  1639  equtr2  1641  equequ2  1643  elequ1  1644  elequ2  1645  ax10o  1647  cbvalh  1680  cbvexh  1682  equvini  1685  stdpc7  1697  sbequ12r  1699  sbequ12a  1700  sbequ  1765  sb6rf  1778  sb9v  1899  sb6a  1909  mo2n  1973  cleqh  2184  cbvab  2207  reu8  2802  sbcco2  2851  snnex  4247  tfisi  4377  opeliunxp  4463  elrnmpt1  4656  rnxpid  4833  iotaval  4959  elabrex  5500  opabex3d  5851  opabex3  5852  enq0ref  6939  setindis  11331  bdsetindis  11333
  Copyright terms: Public domain W3C validator