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

Theorem sylancom 649
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 448 . 2  |-  ( (
ph  /\  ps )  ->  ps )
3 sylancom.2 . 2  |-  ( ( ch  /\  ps )  ->  th )
41, 2, 3syl2anc 643 1  |-  ( (
ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ordin  4603  sofld  5310  fimacnvdisj  5613  wemoiso  6070  wemoiso2  6071  smorndom  6622  rdglim  6676  oaabs  6879  onomeneq  7288  domfi  7322  brwdom2  7533  infdiffi  7604  cantnflem1  7637  wemapwe  7646  cnfcom3lem  7652  r1lim  7690  carduni  7860  ac5num  7909  infunsdom1  8085  cofsmo  8141  isf32lem6  8230  hsmexlem1  8298  ac6c4  8353  pwfseqlem1  8525  tskuni  8650  recgt1i  9899  avgle2  10200  uzindOLD  10356  rpnnen1lem1  10592  ioodisj  11018  fzneuz  11120  hasheni  11624  hashun2  11649  reccn2  12382  isershft  12449  sumeq2ii  12479  demoivreALT  12794  xpnnenOLD  12801  bitsp1  12935  gcdneg  13018  eucalginv  13067  eucalg  13070  odzdvds  13173  fldivp1  13258  prmunb  13274  vdwap1  13337  setsid  13500  acsmapd  14596  symggrp  15095  cntzidss  15128  odmodnn0  15170  sylow2alem1  15243  dvdsrmul1  15750  dvrid  15785  znunit  16836  isphld  16877  cctop  17062  iscnp4  17319  iscncl  17325  cnntr  17331  tx2cn  17634  xkoco1cn  17681  qtopkgen  17734  hmeontr  17793  hmeores  17795  filssufilg  17935  ustuqtop1  18263  ustuqtop2  18264  utop2nei  18272  fmucndlem  18313  cfilufg  18315  metusttoOLD  18579  metustto  18580  cfilucfilOLD  18591  cfilucfil  18592  dscopn  18613  nmoi  18754  iccntr  18844  cphsqrcl2  19141  cmsss  19295  ivthlem3  19342  sca2rab  19400  ovolicc2lem3  19407  evl1val  19940  evl1sca  19942  pf1const  19958  mdegleb  19979  aalioulem3  20243  ulm2  20293  ulmcn  20307  root1eq1  20631  atanlogsublem  20747  birthdaylem3  20784  logexprlim  21001  dchrisumlem3  21177  constr3trllem2  21630  vdgrnn0pnf  21672  eupatrl  21682  grpoidinv  21788  gxadd  21855  rngosn3  22006  imsmetlem  22174  ipasslem1  22324  ip2eqi  22350  hvpncan  22533  pjid  23189  hmopre  23418  eigvalcl  23456  leopnmid  23633  superpos  23849  cvp  23870  ssct  24093  fnct  24097  xlt2addrd  24116  fmcncfil  24309  esumfsup  24452  esumcvg  24468  insiga  24512  ballotlemirc  24781  subfacp1lem6  24863  prodeq2ii  25231  ax5seglem1  25859  ax5seglem2  25860  ax5seglem3a  25861  ax5seglem4  25863  ax5seglem9  25868  ax5seg  25869  axbtwnid  25870  axlowdimlem17  25889  axcontlem2  25896  axcontlem4  25898  axcontlem8  25902  ovoliunnfl  26238  voliunnfl  26240  volsupnfl  26241  ftc1anclem5  26274  indexa  26426  sstotbnd3  26476  heiborlem6  26516  elpell1qr2  26926  oddcomabszz  26998  wepwsolem  27107  mendrng  27468  mendlmod  27469  hausgraph  27499  cncmpmax  27670  stoweidlem7  27723  stoweidlem34  27750  stoweidlem35  27751  stoweidlem49  27765  stoweidlem57  27773  stoweidlem59  27775  stoweidlem60  27776  stoweidlem62  27778  ubmelm1fzo  28110  swrdccatin1  28171  atlatmstc  30054  atlatle  30055  glbconN  30111  intnatN  30141  lnnat  30161  atcvrj2b  30166  atexchcvrN  30174  llncvrlpln  30292  lplncvrlvol  30350  lautcvr  30826  trlatn0  30906  cdleme48fvg  31234  cdlemg33c  31442  dihcl  32005
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 178  df-an 361
  Copyright terms: Public domain W3C validator