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

Theorem equcoms 1795
Description: An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
equcoms.1
Assertion
Ref Expression
equcoms

Proof of Theorem equcoms
StepHypRef Expression
1 equcomi 1793 . 2
2 equcoms.1 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  equtr  1796  stdpc7  1801  equtr2  1802  ax13b  1805  spfw  1806  cbvalw  1808  alcomiw  1811  elequ1  1821  elequ2  1823  19.8a  1857  19.8aOLD  1858  sbequ12r  1993  sbequ12aOLD  1995  cbval  2021  sbequ  2117  sb9  2169  ax13fromc9  2235  axc11-o  2281  euequ1  2288  cleqhOLD  2573  cbvabOLD  2599  reu8  3295  sbcco2  3351  opeliunxp  5056  elrnmpt1  5256  iotaval  5567  fvn0ssdmfun  6022  elabrex  6155  snnex  6606  tfisi  6693  tfinds2  6698  opabex3d  6778  opabex3  6779  mpt2curryd  7017  boxriin  7531  ixpiunwdom  8038  elirrv  8044  rabssnn0fi  12095  imasvscafn  14934  1mavmul  19050  ptbasfi  20082  elmptrab  20328  pcoass  21524  iundisj2  21959  dchrisumlema  23673  dchrisumlem2  23675  cusgrafilem2  24480  frgrancvvdeqlem9  25041  iundisj2f  27449  iundisj2fi  27602  cvmsss2  28719  ax8dfeq  29231  wl-nfs1t  29991  wl-equsb4  30005  wl-ax11-lem8  30032  mblfinlem2  30052  sdclem2  30235  rexzrexnn0  30737  elabrexg  31430  fproddivf  31588  iblsplitf  31769  opeliun2xp  32922  bnj1014  34018  bj-cbvexw  34235  bj-cbvalv  34296  bj-cleqh  34358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator