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

Theorem equcoms 1608
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 1606 . 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 103  ax-gen 1352  ax-ie2 1397  ax-8 1409  ax-17 1433  ax-i9 1437
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  equtr  1609  equtr2  1611  equequ2  1613  elequ1  1614  elequ2  1615  ax10o  1617  cbvalh  1650  cbvexh  1652  equvini  1655  stdpc7  1667  sbequ12r  1669  sbequ12a  1670  sbequ  1735  sb6rf  1747  sb9v  1868  sb6a  1878  mo2n  1942  cleqh  2151  cbvab  2174  reu8  2757  sbcco2  2806  snnex  4206  tfisi  4335  opeliunxp  4420  elrnmpt1  4610  rnxpid  4780  iotaval  4903  elabrex  5422  opabex3d  5773  opabex3  5774  enq0ref  6559  setindis  10422  bdsetindis  10424
  Copyright terms: Public domain W3C validator