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  4422  sofld  5121  fimacnvdisj  5419  wemoiso  5855  wemoiso2  5856  smorndom  6385  rdglim  6439  oaabs  6642  onomeneq  7050  domfi  7084  brwdom2  7287  infdiffi  7358  cantnflem1  7391  wemapwe  7400  cnfcom3lem  7406  r1lim  7444  carduni  7614  ac5num  7663  infunsdom1  7839  cofsmo  7895  isf32lem6  7984  hsmexlem1  8052  ac6c4  8108  pwfseqlem1  8280  tskuni  8405  recgt1i  9653  avgle2  9952  uzindOLD  10106  rpnnen1lem1  10342  ioodisj  10765  fzneuz  10863  hasheni  11347  hashun2  11365  reccn2  12070  isershft  12137  sumeq2ii  12166  demoivreALT  12481  xpnnenOLD  12488  bitsp1  12622  gcdneg  12705  eucalginv  12754  eucalg  12757  odzdvds  12860  fldivp1  12945  prmunb  12961  vdwap1  13024  setsid  13187  acsmapd  14281  symggrp  14780  cntzidss  14813  odmodnn0  14855  sylow2alem1  14928  dvdsrmul1  15435  dvrid  15470  znunit  16517  isphld  16558  cctop  16743  iscncl  16998  cnntr  17004  tx2cn  17304  xkoco1cn  17351  qtopkgen  17401  hmeontr  17460  hmeores  17462  filssufilg  17606  dscopn  18096  nmoi  18237  iccntr  18326  cphsqrcl2  18622  cmsss  18772  ivthlem3  18813  sca2rab  18871  ovolicc2lem3  18878  evl1val  19411  evl1sca  19413  pf1const  19429  mdegleb  19450  aalioulem3  19714  ulm2  19764  ulmcn  19776  root1eq1  20095  atanlogsublem  20211  birthdaylem3  20248  logexprlim  20464  dchrisumlem3  20640  grpoidinv  20875  gxadd  20942  rngosn3  21093  imsmetlem  21259  ipasslem1  21409  ip2eqi  21435  hvpncan  21618  pjid  22274  hmopre  22503  eigvalcl  22541  leopnmid  22718  superpos  22934  cvp  22955  ballotlemirc  23090  xrge0iifiso  23317  ssct  23337  fnct  23341  insiga  23498  subfacp1lem6  23716  ax5seglem1  24556  ax5seglem2  24557  ax5seglem3a  24558  ax5seglem4  24560  ax5seglem9  24565  ax5seg  24566  axbtwnid  24567  axlowdimlem17  24586  axcontlem2  24593  axcontlem4  24595  axcontlem8  24599  surjsec2  25120  iscnp4  25563  domidmor  25948  indexa  26412  sstotbnd3  26500  heiborlem6  26540  elpell1qr2  26957  oddcomabszz  27029  wepwsolem  27138  mendrng  27500  mendlmod  27501  hausgraph  27531  stoweidlem7  27756  atlatmstc  29509  atlatle  29510  glbconN  29566  intnatN  29596  lnnat  29616  atcvrj2b  29621  atexchcvrN  29629  llncvrlpln  29747  lplncvrlvol  29805  lautcvr  30281  trlatn0  30361  cdleme48fvg  30689  cdlemg33c  30897  dihcl  31460
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