Theorem sylancom 678

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

Step	Hyp	Ref	Expression
1		sylancom.1	. 2 |- ( ( ph /\ ps ) -> ch )
2		simpr 467	. 2 |- ( ( ph /\ ps ) -> ps )
3		sylancom.2	. 2 |- ( ( ch /\ ps ) -> th )
4	1, 2, 3	syl2anc 671	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  sofld  5302  ordin  5471  fimacnvdisj  5783  f1oexrnex  6768  wemoiso  6804  wemoiso2  6805  smorndom  7112  rdglim  7169  oaabs  7370  ssct  7678  onomeneq  7787  domfi  7818  f1vrnfibi  7884  brwdom2  8113  infdiffi  8188  cantnflem1  8219  wemapwe  8227  cnfcom3lem  8233  r1lim  8268  carduni  8440  ac5num  8492  infunsdom1  8668  cofsmo  8724  isf32lem6  8813  hsmexlem1  8881  ac6c4  8936  pwfseqlem1  9108  tskuni  9233  recgt1i  10530  avgle2  10881  rpnnen1lem1  11318  ioodisj  11790  fzneuz  11903  mulmod0  12135  hasheni  12562  hashun2  12593  swrdccatin1  12875  reccn2  13708  isershft  13775  sumeq2ii  13807  prodeq2ii  14015  demoivreALT  14303  bitsp1  14452  gcdneg  14538  eucalginv  14591  eucalg  14594  odzdvds  14788  odzdvdsOLD  14794  fldivp1  14890  prmunb  14906  vdwap1  14975  setsid  15212  funcsetcestrclem7  16094  acsmapd  16472  intopsn  16546  cntzidss  17039  symggrp  17089  odmodnn0  17237  sylow2alem1  17317  telgsumfzs  17667  dprdsn  17717  dvdsrmul1  17929  dvrid  17964  evl1val  18965  evl1sca  18970  pf1const  18982  znunit  19182  isphld  19269  frlmup1  19404  mat1f1o  19551  mat1mhm  19557  matunit  19751  pm2mpmhmlem2  19891  cctop  20069  iscnp4  20327  iscncl  20333  cnntr  20339  tx2cn  20673  xkoco1cn  20720  qtopkgen  20773  hmeontr  20832  hmeores  20834  filssufilg  20974  ustuqtop1  21304  ustuqtop2  21305  utop2nei  21313  fmucndlem  21354  cfilufg  21356  xmetres2  21424  metres2  21426  metustto  21616  cfilucfil  21622  dscopn  21636  nmoi  21781  nmoiOLD  21797  iccntr  21887  cphsqrtcl2  22212  cmsss  22366  ivthlem3  22452  sca2rab  22513  ovolicc2lem3  22520  mdegleb  23061  aalioulem3  23338  ulm2  23388  ulmcn  23402  root1eq1  23743  atanlogsublem  23889  birthdaylem3  23927  logexprlim  24201  dchrisumlem3  24377  tglowdim1i  24593  f1otrg  24949  f1otrge  24950  ax5seglem1  25006  ax5seglem2  25007  ax5seglem3a  25008  ax5seglem4  25010  ax5seglem9  25015  ax5seg  25016  axbtwnid  25017  axlowdimlem17  25036  axcontlem2  25043  axcontlem4  25045  axcontlem8  25049  constr3trllem2  25427  vdgrnn0pnf  25685  rusgranumwlks  25732  eupatrl  25744  grpoidinv  25984  gxadd  26051  rngosn3  26202  imsmetlem  26370  ipasslem1  26520  ip2eqi  26546  hvpncan  26740  pjid  27396  hmopre  27624  eigvalcl  27662  leopnmid  27839  superpos  28055  cvp  28076  rabfodom  28188  fnct  28345  xlt2addrd  28386  lmodslmd  28568  locfinreflem  28715  prsdm  28768  prsrn  28769  fmcncfil  28785  rge0scvg  28803  esumfsup  28939  esumcvg  28955  insiga  29007  ballotlemirc  29412  ballotlemircOLD  29450  eluzmn  29471  signstfvcl  29510  subfacp1lem6  29956  msubff1  30242  fv2ndcnv  30471  ovoliunnfl  32026  voliunnfl  32028  volsupnfl  32029  ftc1anclem5  32065  indexa  32104  sstotbnd3  32152  heiborlem6  32192  atlatmstc  32929  atlatle  32930  glbconN  32986  intnatN  33016  lnnat  33036  atcvrj2b  33041  atexchcvrN  33049  llncvrlpln  33167  lplncvrlvol  33225  lautcvr  33701  trlatn0  33782  cdleme48fvg  34111  cdlemg33c  34319  dihcl  34882  elpell1qr2  35762  oddcomabszz  35836  wepwsolem  35944  mendring  36102  mendlmod  36103  hausgraph  36133  rp-isfinite5  36206  cncmpmax  37392  adant423  37406  icccncfext  37802  dvnprodlem2  37859  stoweidlem7  37904  stoweidlem34  37932  stoweidlem35  37933  stoweidlem59  37957  stoweidlem60  37958  stoweidlem62  37960  stoweidlem62OLD  37961  fourierdlem34  38041  fourierdlem73  38080  fourierdlem77  38084  etransclem35  38171  pgrple2abl  40422