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

Theorem equcoms 1576
 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 (x = yφ)
Assertion
Ref Expression
equcoms (y = xφ)

Proof of Theorem equcoms
StepHypRef Expression
1 equcomi 1574 . 2 (y = xx = y)
2 equcoms.1 . 2 (x = yφ)
31, 2syl 14 1 (y = xφ)
 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 1318  ax-ie2 1364  ax-8 1376  ax-17 1400  ax-i9 1404 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  equtr  1577  equtr2  1579  equequ2  1581  elequ1  1582  elequ2  1583  ax10o  1585  cbvalh  1618  cbvexh  1620  equvini  1623  stdpc7  1635  sbequ12r  1637  sbequ12a  1638  sbequ  1703  sb6rf  1715  sb9v  1836  sb6a  1846  mo2n  1910  cleqh  2119  cbvab  2142  reu8  2714  sbcco2  2763  snnex  4131  tfisi  4237  opeliunxp  4322  elrnmpt1  4512  rnxpid  4682  iotaval  4805  elabrex  5322  opabex3d  5671  opabex3  5672  enq0ref  6288  setindis  7332  bdsetindis  7334
 Copyright terms: Public domain W3C validator