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

Theorem sylancom 667
Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)
Hypotheses
Ref Expression
sylancom.1
sylancom.2
Assertion
Ref Expression
sylancom

Proof of Theorem sylancom
StepHypRef Expression
1 sylancom.1 . 2
2 simpr 461 . 2
3 sylancom.2 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  ordin  4913  sofld  5460  fimacnvdisj  5768  f1oexrnex  6749  wemoiso  6785  wemoiso2  6786  smorndom  7058  rdglim  7111  oaabs  7312  onomeneq  7727  domfi  7761  brwdom2  8020  infdiffi  8095  cantnflem1  8129  cantnflem1OLD  8152  wemapwe  8160  wemapweOLD  8161  cnfcom3lem  8168  cnfcom3lemOLD  8176  r1lim  8211  carduni  8383  ac5num  8438  infunsdom1  8614  cofsmo  8670  isf32lem6  8759  hsmexlem1  8827  ac6c4  8882  pwfseqlem1  9057  tskuni  9182  recgt1i  10467  avgle2  10804  uzindOLD  10982  rpnnen1lem1  11237  ioodisj  11679  fzneuz  11788  hasheni  12421  hashun2  12451  swrdccatin1  12708  reccn2  13419  isershft  13486  sumeq2ii  13515  prodeq2ii  13720  demoivreALT  13936  xpnnenOLD  13943  bitsp1  14081  gcdneg  14164  eucalginv  14213  eucalg  14216  odzdvds  14322  fldivp1  14416  prmunb  14432  vdwap1  14495  setsid  14673  acsmapd  15808  intopsn  15882  cntzidss  16375  symggrp  16425  odmodnn0  16564  sylow2alem1  16637  telgsumfzs  17018  dprdsn  17083  dvdsrmul1  17302  dvrid  17337  evl1val  18365  evl1sca  18370  pf1const  18382  znunit  18602  isphld  18689  frlmup1  18832  mat1f1o  18980  mat1mhm  18986  matunit  19180  pm2mpmhmlem2  19320  cctop  19507  iscnp4  19764  iscncl  19770  cnntr  19776  tx2cn  20111  xkoco1cn  20158  qtopkgen  20211  hmeontr  20270  hmeores  20272  filssufilg  20412  ustuqtop1  20744  ustuqtop2  20745  utop2nei  20753  fmucndlem  20794  cfilufg  20796  xmetres2  20864  metres2  20866  metusttoOLD  21060  metustto  21061  cfilucfilOLD  21072  cfilucfil  21073  dscopn  21094  nmoi  21235  iccntr  21326  cphsqrtcl2  21633  cmsss  21789  ivthlem3  21865  sca2rab  21923  ovolicc2lem3  21930  mdegleb  22464  aalioulem3  22730  ulm2  22780  ulmcn  22794  root1eq1  23129  atanlogsublem  23246  birthdaylem3  23283  logexprlim  23500  dchrisumlem3  23676  tglowdim1i  23892  f1otrg  24174  f1otrge  24175  ax5seglem1  24231  ax5seglem2  24232  ax5seglem3a  24233  ax5seglem4  24235  ax5seglem9  24240  ax5seg  24241  axbtwnid  24242  axlowdimlem17  24261  axcontlem2  24268  axcontlem4  24270  axcontlem8  24274  constr3trllem2  24651  vdgrnn0pnf  24909  rusgranumwlks  24956  eupatrl  24968  grpoidinv  25210  gxadd  25277  rngosn3  25428  imsmetlem  25596  ipasslem1  25746  ip2eqi  25772  hvpncan  25956  pjid  26613  hmopre  26842  eigvalcl  26880  leopnmid  27057  superpos  27273  cvp  27294  rabfodom  27404  ssct  27532  fnct  27536  xlt2addrd  27578  lmodslmd  27747  locfinreflem  27843  prsdm  27896  prsrn  27897  fmcncfil  27913  rge0scvg  27931  esumfsup  28076  esumcvg  28092  insiga  28137  ballotlemirc  28470  eluzmn  28491  signstfvcl  28530  subfacp1lem6  28629  msubff1  28916  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  ftc1anclem5  30094  indexa  30224  sstotbnd3  30272  heiborlem6  30312  elpell1qr2  30808  oddcomabszz  30880  wepwsolem  30987  mendring  31141  mendlmod  31142  hausgraph  31172  cncmpmax  31407  adant423  31425  icccncfext  31690  dvnprodlem2  31744  stoweidlem7  31789  stoweidlem34  31816  stoweidlem35  31817  stoweidlem59  31841  stoweidlem60  31842  stoweidlem62  31844  fourierdlem34  31923  fourierdlem73  31962  fourierdlem77  31966  etransclem35  32052  f1vrnfibi  32313  funcsetcestrclem7  32667  pgrple2abl  32958  atlatmstc  35044  atlatle  35045  glbconN  35101  intnatN  35131  lnnat  35151  atcvrj2b  35156  atexchcvrN  35164  llncvrlpln  35282  lplncvrlvol  35340  lautcvr  35816  trlatn0  35897  cdleme48fvg  36226  cdlemg33c  36434  dihcl  36997  rp-isfinite5  37743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator