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

Theorem equcoms 1591
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 1589 . 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 1335  ax-ie2 1380  ax-8 1392  ax-17 1416  ax-i9 1420
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  equtr  1592  equtr2  1594  equequ2  1596  elequ1  1597  elequ2  1598  ax10o  1600  cbvalh  1633  cbvexh  1635  equvini  1638  stdpc7  1650  sbequ12r  1652  sbequ12a  1653  sbequ  1718  sb6rf  1730  sb9v  1851  sb6a  1861  mo2n  1925  cleqh  2134  cbvab  2157  reu8  2731  sbcco2  2780  snnex  4147  tfisi  4253  opeliunxp  4338  elrnmpt1  4528  rnxpid  4698  iotaval  4821  elabrex  5340  opabex3d  5690  opabex3  5691  enq0ref  6415  setindis  9351  bdsetindis  9353
  Copyright terms: Public domain W3C validator