Theorem sylancom 667

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

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  ordin  4908  sofld  5453  fimacnvdisj  5761  f1oexrnex  6730  wemoiso  6766  wemoiso2  6767  smorndom  7036  rdglim  7089  oaabs  7290  onomeneq  7704  domfi  7738  brwdom2  7995  infdiffi  8070  cantnflem1  8104  cantnflem1OLD  8127  wemapwe  8135  wemapweOLD  8136  cnfcom3lem  8143  cnfcom3lemOLD  8151  r1lim  8186  carduni  8358  ac5num  8413  infunsdom1  8589  cofsmo  8645  isf32lem6  8734  hsmexlem1  8802  ac6c4  8857  pwfseqlem1  9032  tskuni  9157  recgt1i  10438  avgle2  10775  uzindOLD  10951  rpnnen1lem1  11204  ioodisj  11646  fzneuz  11755  hasheni  12385  hashun2  12415  swrdccatin1  12667  reccn2  13378  isershft  13445  sumeq2ii  13474  demoivreALT  13793  xpnnenOLD  13800  bitsp1  13936  gcdneg  14019  eucalginv  14068  eucalg  14071  odzdvds  14177  fldivp1  14271  prmunb  14287  vdwap1  14350  setsid  14527  acsmapd  15661  cntzidss  16170  symggrp  16220  odmodnn0  16360  sylow2alem1  16433  telgsumfzs  16809  dvdsrmul1  17086  dvrid  17121  evl1val  18136  evl1sca  18141  pf1const  18153  znunit  18369  isphld  18456  frlmup1  18599  mat1f1o  18747  mat1mhm  18753  matunit  18947  pm2mpmhmlem2  19087  cctop  19273  iscnp4  19530  iscncl  19536  cnntr  19542  tx2cn  19846  xkoco1cn  19893  qtopkgen  19946  hmeontr  20005  hmeores  20007  filssufilg  20147  ustuqtop1  20479  ustuqtop2  20480  utop2nei  20488  fmucndlem  20529  cfilufg  20531  metusttoOLD  20795  metustto  20796  cfilucfilOLD  20807  cfilucfil  20808  dscopn  20829  nmoi  20970  iccntr  21061  cphsqrtcl2  21368  cmsss  21524  ivthlem3  21600  sca2rab  21658  ovolicc2lem3  21665  mdegleb  22199  aalioulem3  22464  ulm2  22514  ulmcn  22528  root1eq1  22857  atanlogsublem  22974  birthdaylem3  23011  logexprlim  23228  dchrisumlem3  23404  ax5seglem1  23907  ax5seglem2  23908  ax5seglem3a  23909  ax5seglem4  23911  ax5seglem9  23916  ax5seg  23917  axbtwnid  23918  axlowdimlem17  23937  axcontlem2  23944  axcontlem4  23946  axcontlem8  23950  constr3trllem2  24327  vdgrnn0pnf  24585  rusgranumwlks  24632  eupatrl  24644  grpoidinv  24886  gxadd  24953  rngosn3  25104  imsmetlem  25272  ipasslem1  25422  ip2eqi  25448  hvpncan  25632  pjid  26289  hmopre  26518  eigvalcl  26556  leopnmid  26733  superpos  26949  cvp  26970  ssct  27204  fnct  27208  xlt2addrd  27246  ordtconlem1  27542  fmcncfil  27549  esumfsup  27716  esumcvg  27732  insiga  27777  ballotlemirc  28110  signswch  28158  signstfvneq0  28169  signstfvcl  28170  subfacp1lem6  28269  prodeq2ii  28622  ovoliunnfl  29633  voliunnfl  29635  volsupnfl  29636  ftc1anclem5  29671  indexa  29827  sstotbnd3  29875  heiborlem6  29915  elpell1qr2  30412  oddcomabszz  30484  wepwsolem  30591  mendrng  30746  mendlmod  30747  hausgraph  30777  cncmpmax  30985  dvasinbx  31250  stoweidlem7  31307  stoweidlem34  31334  stoweidlem35  31335  stoweidlem49  31349  stoweidlem57  31357  stoweidlem59  31359  stoweidlem60  31360  stoweidlem62  31362  fourierdlem15  31422  fourierdlem95  31502  f1vrnfibi  31782  pgrple2abl  32023  atlatmstc  34116  atlatle  34117  glbconN  34173  intnatN  34203  lnnat  34223  atcvrj2b  34228  atexchcvrN  34236  llncvrlpln  34354  lplncvrlvol  34412  lautcvr  34888  trlatn0  34968  cdleme48fvg  35296  cdlemg33c  35504  dihcl  36067