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

Theorem equcoms 1570
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 1568 . 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 1314  ax-ie2 1359  ax-8 1371  ax-17 1395  ax-i9 1399
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  equtr  1571  equtr2  1573  equequ2  1575  elequ1  1576  elequ2  1577  ax10o  1579  cbvalh  1612  cbvexh  1614  equvini  1617  stdpc7  1629  sbequ12r  1631  sbequ12a  1632  sbequ  1697  sb6rf  1709  sb9v  1830  sb6a  1840  mo2n  1904  cleqh  2113  cbvab  2136  reu8  2708  sbcco2  2757  snnex  4122  tfisi  4228  opeliunxp  4313  elrnmpt1  4503  rnxpid  4673  iotaval  4796  elabrex  5313  opabex3d  5662  opabex3  5663  enq0ref  6277  setindis  8603  bdsetindis  8605
  Copyright terms: Public domain W3C validator