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

Theorem equcoms 1669
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 1665 . 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 105  ax-gen 1410  ax-ie2 1455  ax-8 1467  ax-17 1491  ax-i9 1495
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  equtr  1670  equtr2  1672  equequ2  1674  elequ1  1675  elequ2  1676  ax10o  1678  cbvalh  1711  cbvexh  1713  equvini  1716  stdpc7  1728  sbequ12r  1730  sbequ12a  1731  sbequ  1796  sb6rf  1809  sb9v  1931  sb6a  1941  mo2n  2005  cleqh  2217  cbvab  2240  sbralie  2644  reu8  2853  sbcco2  2904  snnex  4339  tfisi  4471  opeliunxp  4564  elrnmpt1  4760  rnxpid  4943  iotaval  5069  elabrex  5627  opabex3d  5987  opabex3  5988  enq0ref  7209  setindis  13061  bdsetindis  13063
  Copyright terms: Public domain W3C validator