Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  equcoms Structured version   Unicode version

Theorem equcoms 1694
 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 1692 . 2
2 equcoms.1 . 2
31, 2syl 16 1
 Colors of variables: wff set class Syntax hints:   wi 4 This theorem is referenced by:  equtr  1695  equtr2  1701  ax12b  1702  ax12bOLD  1703  spfw  1704  spwOLD  1708  cbvalw  1715  cbvalvwOLD  1717  alcomiw  1719  elequ1  1729  elequ2  1731  19.8a  1763  stdpc7  1943  sbequ12r  1946  sbequ12a  1947  a9e  1953  cbval  1983  ax12OLD  2021  ax10oOLD  2040  equvini  2084  equviniOLD  2085  sbequi  2112  sbequ  2113  sb6rf  2169  sb6a  2195  ax12from12o  2235  ax10o-o  2282  mo  2305  cleqh  2535  cbvab  2556  reu8  3132  sbcco2  3186  snnex  4715  tfisi  4840  tfinds2  4845  opeliunxp  4931  elrnmpt1  5121  iotaval  5431  elabrex  5987  opabex3d  5991  opabex3  5992  boxriin  7106  ixpiunwdom  7561  elirrv  7567  imasvscafn  13764  ptbasfi  17615  elmptrab  17861  pcoass  19051  iundisj2  19445  dchrisumlema  21184  dchrisumlem2  21186  cusgrafilem2  21491  iundisj2f  24032  iundisj2fi  24155  voliune  24587  volfiniune  24588  cvmsss2  24963  ax13dfeq  25428  mblfinlem2  26246  sdclem2  26448  rexzrexnn0  26866  frgrancvvdeqlem9  28492  bnj1014  29393  ax10oNEW7  29538  cbvalwwAUX7  29581  equviniNEW7  29589  sbequNEW7  29642  sb6rfNEW7  29654  sb6aNEW7  29673  cbvalOLD7  29787 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688 This theorem depends on definitions:  df-bi 179  df-ex 1552
 Copyright terms: Public domain W3C validator