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

Theorem equcoms 1594
 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 1592 . 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 99  ax-gen 1338  ax-ie2 1383  ax-8 1395  ax-17 1419  ax-i9 1423 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  equtr  1595  equtr2  1597  equequ2  1599  elequ1  1600  elequ2  1601  ax10o  1603  cbvalh  1636  cbvexh  1638  equvini  1641  stdpc7  1653  sbequ12r  1655  sbequ12a  1656  sbequ  1721  sb6rf  1733  sb9v  1854  sb6a  1864  mo2n  1928  cleqh  2137  cbvab  2160  reu8  2737  sbcco2  2786  snnex  4181  tfisi  4310  opeliunxp  4395  elrnmpt1  4585  rnxpid  4755  iotaval  4878  elabrex  5397  opabex3d  5748  opabex3  5749  enq0ref  6531  setindis  10092  bdsetindis  10094
 Copyright terms: Public domain W3C validator