Theorem sylancom 671

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 462	. 2 |- ( ( ph /\ ps ) -> ps )
3		sylancom.2	. 2 |- ( ( ch /\ ps ) -> th )
4	1, 2, 3	syl2anc 665	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  sofld  5300  ordin  5469  fimacnvdisj  5775  f1oexrnex  6753  wemoiso  6789  wemoiso2  6790  smorndom  7092  rdglim  7149  oaabs  7350  onomeneq  7765  domfi  7796  f1vrnfibi  7862  brwdom2  8091  infdiffi  8165  cantnflem1  8196  wemapwe  8204  cnfcom3lem  8210  r1lim  8245  carduni  8417  ac5num  8468  infunsdom1  8644  cofsmo  8700  isf32lem6  8789  hsmexlem1  8857  ac6c4  8912  pwfseqlem1  9084  tskuni  9209  recgt1i  10504  avgle2  10854  rpnnen1lem1  11291  ioodisj  11763  fzneuz  11876  mulmod0  12104  hasheni  12531  hashun2  12562  swrdccatin1  12830  reccn2  13648  isershft  13715  sumeq2ii  13747  prodeq2ii  13955  demoivreALT  14243  bitsp1  14392  gcdneg  14478  eucalginv  14531  eucalg  14534  odzdvds  14728  odzdvdsOLD  14734  fldivp1  14830  prmunb  14846  vdwap1  14915  setsid  15152  funcsetcestrclem7  16034  acsmapd  16412  intopsn  16486  cntzidss  16979  symggrp  17029  odmodnn0  17177  sylow2alem1  17257  telgsumfzs  17607  dprdsn  17657  dvdsrmul1  17869  dvrid  17904  evl1val  18905  evl1sca  18910  pf1const  18922  znunit  19121  isphld  19208  frlmup1  19343  mat1f1o  19490  mat1mhm  19496  matunit  19690  pm2mpmhmlem2  19830  cctop  20008  iscnp4  20266  iscncl  20272  cnntr  20278  tx2cn  20612  xkoco1cn  20659  qtopkgen  20712  hmeontr  20771  hmeores  20773  filssufilg  20913  ustuqtop1  21243  ustuqtop2  21244  utop2nei  21252  fmucndlem  21293  cfilufg  21295  xmetres2  21363  metres2  21365  metustto  21555  cfilucfil  21561  dscopn  21575  nmoi  21720  nmoiOLD  21736  iccntr  21826  cphsqrtcl2  22151  cmsss  22305  ivthlem3  22391  sca2rab  22452  ovolicc2lem3  22459  mdegleb  23000  aalioulem3  23277  ulm2  23327  ulmcn  23341  root1eq1  23682  atanlogsublem  23828  birthdaylem3  23866  logexprlim  24140  dchrisumlem3  24316  tglowdim1i  24532  f1otrg  24888  f1otrge  24889  ax5seglem1  24945  ax5seglem2  24946  ax5seglem3a  24947  ax5seglem4  24949  ax5seglem9  24954  ax5seg  24955  axbtwnid  24956  axlowdimlem17  24975  axcontlem2  24982  axcontlem4  24984  axcontlem8  24988  constr3trllem2  25365  vdgrnn0pnf  25623  rusgranumwlks  25670  eupatrl  25682  grpoidinv  25922  gxadd  25989  rngosn3  26140  imsmetlem  26308  ipasslem1  26458  ip2eqi  26484  hvpncan  26678  pjid  27334  hmopre  27562  eigvalcl  27600  leopnmid  27777  superpos  27993  cvp  28014  rabfodom  28127  ssct  28287  fnct  28291  xlt2addrd  28332  lmodslmd  28515  locfinreflem  28663  prsdm  28716  prsrn  28717  fmcncfil  28733  rge0scvg  28751  esumfsup  28887  esumcvg  28903  insiga  28955  ballotlemirc  29360  ballotlemircOLD  29398  eluzmn  29419  signstfvcl  29458  subfacp1lem6  29904  msubff1  30190  fv2ndcnv  30418  ovoliunnfl  31896  voliunnfl  31898  volsupnfl  31899  ftc1anclem5  31935  indexa  31974  sstotbnd3  32022  heiborlem6  32062  atlatmstc  32804  atlatle  32805  glbconN  32861  intnatN  32891  lnnat  32911  atcvrj2b  32916  atexchcvrN  32924  llncvrlpln  33042  lplncvrlvol  33100  lautcvr  33576  trlatn0  33657  cdleme48fvg  33986  cdlemg33c  34194  dihcl  34757  elpell1qr2  35638  oddcomabszz  35712  wepwsolem  35820  mendring  35978  mendlmod  35979  hausgraph  36009  rp-isfinite5  36082  cncmpmax  37214  adant423  37228  icccncfext  37585  dvnprodlem2  37642  stoweidlem7  37687  stoweidlem34  37715  stoweidlem35  37716  stoweidlem59  37740  stoweidlem60  37741  stoweidlem62  37743  stoweidlem62OLD  37744  fourierdlem34  37824  fourierdlem73  37863  fourierdlem77  37867  etransclem35  37954  pgrple2abl  39424