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  4895  sofld  5442  fimacnvdisj  5750  f1oexrnex  6731  wemoiso  6767  wemoiso2  6768  smorndom  7038  rdglim  7091  oaabs  7292  onomeneq  7706  domfi  7740  brwdom2  7999  infdiffi  8074  cantnflem1  8108  cantnflem1OLD  8131  wemapwe  8139  wemapweOLD  8140  cnfcom3lem  8147  cnfcom3lemOLD  8155  r1lim  8190  carduni  8362  ac5num  8417  infunsdom1  8593  cofsmo  8649  isf32lem6  8738  hsmexlem1  8806  ac6c4  8861  pwfseqlem1  9036  tskuni  9161  recgt1i  10445  avgle2  10782  uzindOLD  10960  rpnnen1lem1  11214  ioodisj  11656  fzneuz  11765  hasheni  12397  hashun2  12427  swrdccatin1  12684  reccn2  13395  isershft  13462  sumeq2ii  13491  demoivreALT  13810  xpnnenOLD  13817  bitsp1  13955  gcdneg  14038  eucalginv  14087  eucalg  14090  odzdvds  14196  fldivp1  14290  prmunb  14306  vdwap1  14369  setsid  14547  acsmapd  15679  intopsn  15753  cntzidss  16246  symggrp  16296  odmodnn0  16435  sylow2alem1  16508  telgsumfzs  16889  dprdsn  16954  dvdsrmul1  17173  dvrid  17208  evl1val  18236  evl1sca  18241  pf1const  18253  znunit  18472  isphld  18559  frlmup1  18702  mat1f1o  18850  mat1mhm  18856  matunit  19050  pm2mpmhmlem2  19190  cctop  19377  iscnp4  19634  iscncl  19640  cnntr  19646  tx2cn  19981  xkoco1cn  20028  qtopkgen  20081  hmeontr  20140  hmeores  20142  filssufilg  20282  ustuqtop1  20614  ustuqtop2  20615  utop2nei  20623  fmucndlem  20664  cfilufg  20666  xmetres2  20734  metres2  20736  metusttoOLD  20930  metustto  20931  cfilucfilOLD  20942  cfilucfil  20943  dscopn  20964  nmoi  21105  iccntr  21196  cphsqrtcl2  21503  cmsss  21659  ivthlem3  21735  sca2rab  21793  ovolicc2lem3  21800  mdegleb  22334  aalioulem3  22599  ulm2  22649  ulmcn  22663  root1eq1  22998  atanlogsublem  23115  birthdaylem3  23152  logexprlim  23369  dchrisumlem3  23545  tglowdim1i  23761  f1otrg  24043  f1otrge  24044  ax5seglem1  24100  ax5seglem2  24101  ax5seglem3a  24102  ax5seglem4  24104  ax5seglem9  24109  ax5seg  24110  axbtwnid  24111  axlowdimlem17  24130  axcontlem2  24137  axcontlem4  24139  axcontlem8  24143  constr3trllem2  24520  vdgrnn0pnf  24778  rusgranumwlks  24825  eupatrl  24837  grpoidinv  25079  gxadd  25146  rngosn3  25297  imsmetlem  25465  ipasslem1  25615  ip2eqi  25641  hvpncan  25825  pjid  26482  hmopre  26711  eigvalcl  26749  leopnmid  26926  superpos  27142  cvp  27163  rabfodom  27273  ssct  27401  fnct  27405  xlt2addrd  27447  lmodslmd  27617  locfinreflem  27713  prsdm  27766  prsrn  27767  fmcncfil  27783  rge0scvg  27801  esumfsup  27946  esumcvg  27962  insiga  28007  ballotlemirc  28340  eluzmn  28361  signstfvcl  28400  subfacp1lem6  28499  msubff1  28786  prodeq2ii  29017  ovoliunnfl  30028  voliunnfl  30030  volsupnfl  30031  ftc1anclem5  30066  indexa  30196  sstotbnd3  30244  heiborlem6  30284  elpell1qr2  30780  oddcomabszz  30852  wepwsolem  30959  mendring  31114  mendlmod  31115  hausgraph  31145  cncmpmax  31358  adant423  31379  icccncfext  31597  stoweidlem7  31678  stoweidlem34  31705  stoweidlem35  31706  stoweidlem59  31730  stoweidlem60  31731  stoweidlem62  31733  fourierdlem34  31812  fourierdlem73  31851  fourierdlem77  31855  f1vrnfibi  32151  pgrple2abl  32686  atlatmstc  34767  atlatle  34768  glbconN  34824  intnatN  34854  lnnat  34874  atcvrj2b  34879  atexchcvrN  34887  llncvrlpln  35005  lplncvrlvol  35063  lautcvr  35539  trlatn0  35620  cdleme48fvg  35949  cdlemg33c  36157  dihcl  36720  rp-isfinite5  37429