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

Theorem sylancom 648
Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.)
Hypotheses
Ref Expression
sylancom.1  |-  ( (
ph  /\  ps )  ->  ch )
sylancom.2  |-  ( ( ch  /\  ps )  ->  th )
Assertion
Ref Expression
sylancom  |-  ( (
ph  /\  ps )  ->  th )

Proof of Theorem sylancom
StepHypRef Expression
1 sylancom.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
2 simpr 447 . 2  |-  ( (
ph  /\  ps )  ->  ps )
3 sylancom.2 . 2  |-  ( ( ch  /\  ps )  ->  th )
41, 2, 3syl2anc 642 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ordin  4438  sofld  5137  fimacnvdisj  5435  wemoiso  5871  wemoiso2  5872  smorndom  6401  rdglim  6455  oaabs  6658  onomeneq  7066  domfi  7100  brwdom2  7303  infdiffi  7374  cantnflem1  7407  wemapwe  7416  cnfcom3lem  7422  r1lim  7460  carduni  7630  ac5num  7679  infunsdom1  7855  cofsmo  7911  isf32lem6  8000  hsmexlem1  8068  ac6c4  8124  pwfseqlem1  8296  tskuni  8421  recgt1i  9669  avgle2  9968  uzindOLD  10122  rpnnen1lem1  10358  ioodisj  10781  fzneuz  10879  hasheni  11363  hashun2  11381  reccn2  12086  isershft  12153  sumeq2ii  12182  demoivreALT  12497  xpnnenOLD  12504  bitsp1  12638  gcdneg  12721  eucalginv  12770  eucalg  12773  odzdvds  12876  fldivp1  12961  prmunb  12977  vdwap1  13040  setsid  13203  acsmapd  14297  symggrp  14796  cntzidss  14829  odmodnn0  14871  sylow2alem1  14944  dvdsrmul1  15451  dvrid  15486  znunit  16533  isphld  16574  cctop  16759  iscncl  17014  cnntr  17020  tx2cn  17320  xkoco1cn  17367  qtopkgen  17417  hmeontr  17476  hmeores  17478  filssufilg  17622  dscopn  18112  nmoi  18253  iccntr  18342  cphsqrcl2  18638  cmsss  18788  ivthlem3  18829  sca2rab  18887  ovolicc2lem3  18894  evl1val  19427  evl1sca  19429  pf1const  19445  mdegleb  19466  aalioulem3  19730  ulm2  19780  ulmcn  19792  root1eq1  20111  atanlogsublem  20227  birthdaylem3  20264  logexprlim  20480  dchrisumlem3  20656  grpoidinv  20891  gxadd  20958  rngosn3  21109  imsmetlem  21275  ipasslem1  21425  ip2eqi  21451  hvpncan  21634  pjid  22290  hmopre  22519  eigvalcl  22557  leopnmid  22734  superpos  22950  cvp  22971  ballotlemirc  23106  xrge0iifiso  23332  ssct  23352  fnct  23356  insiga  23513  subfacp1lem6  23731  cprodeq2ii  24135  ax5seglem1  24628  ax5seglem2  24629  ax5seglem3a  24630  ax5seglem4  24632  ax5seglem9  24637  ax5seg  24638  axbtwnid  24639  axlowdimlem17  24658  axcontlem2  24665  axcontlem4  24667  axcontlem8  24671  ovoliunnfl  25001  surjsec2  25223  iscnp4  25666  domidmor  26051  indexa  26515  sstotbnd3  26603  heiborlem6  26643  elpell1qr2  27060  oddcomabszz  27132  wepwsolem  27241  mendrng  27603  mendlmod  27604  hausgraph  27634  stoweidlem7  27859  eupatrl  28385  constr3trllem2  28397  atlatmstc  30131  atlatle  30132  glbconN  30188  intnatN  30218  lnnat  30238  atcvrj2b  30243  atexchcvrN  30251  llncvrlpln  30369  lplncvrlvol  30427  lautcvr  30903  trlatn0  30983  cdleme48fvg  31311  cdlemg33c  31519  dihcl  32082
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator