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

Theorem equcoms 1636
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 1633 . 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 1379  ax-ie2 1424  ax-8 1436  ax-17 1460  ax-i9 1464
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  equtr  1637  equtr2  1639  equequ2  1641  elequ1  1642  elequ2  1643  ax10o  1645  cbvalh  1678  cbvexh  1680  equvini  1683  stdpc7  1695  sbequ12r  1697  sbequ12a  1698  sbequ  1763  sb6rf  1776  sb9v  1897  sb6a  1907  mo2n  1971  cleqh  2182  cbvab  2205  reu8  2797  sbcco2  2846  snnex  4227  tfisi  4356  opeliunxp  4441  elrnmpt1  4633  rnxpid  4805  iotaval  4928  elabrex  5449  opabex3d  5799  opabex3  5800  enq0ref  6737  setindis  11029  bdsetindis  11031
  Copyright terms: Public domain W3C validator