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  4744  sofld  5281  fimacnvdisj  5584  f1oexrnex  6522  wemoiso  6557  wemoiso2  6558  smorndom  6821  rdglim  6874  oaabs  7075  onomeneq  7492  domfi  7526  brwdom2  7780  infdiffi  7855  cantnflem1  7889  cantnflem1OLD  7912  wemapwe  7920  wemapweOLD  7921  cnfcom3lem  7928  cnfcom3lemOLD  7936  r1lim  7971  carduni  8143  ac5num  8198  infunsdom1  8374  cofsmo  8430  isf32lem6  8519  hsmexlem1  8587  ac6c4  8642  pwfseqlem1  8817  tskuni  8942  recgt1i  10221  avgle2  10557  uzindOLD  10728  rpnnen1lem1  10971  ioodisj  11407  fzneuz  11533  hasheni  12111  hashun2  12138  swrdccatin1  12366  reccn2  13066  isershft  13133  sumeq2ii  13162  demoivreALT  13477  xpnnenOLD  13484  bitsp1  13619  gcdneg  13702  eucalginv  13751  eucalg  13754  odzdvds  13859  fldivp1  13951  prmunb  13967  vdwap1  14030  setsid  14207  acsmapd  15340  cntzidss  15846  symggrp  15896  odmodnn0  16034  sylow2alem1  16107  dvdsrmul1  16733  dvrid  16768  evl1val  17738  evl1sca  17743  pf1const  17755  znunit  17971  isphld  18058  frlmup1  18201  matunit  18459  cctop  18585  iscnp4  18842  iscncl  18848  cnntr  18854  tx2cn  19158  xkoco1cn  19205  qtopkgen  19258  hmeontr  19317  hmeores  19319  filssufilg  19459  ustuqtop1  19791  ustuqtop2  19792  utop2nei  19800  fmucndlem  19841  cfilufg  19843  metusttoOLD  20107  metustto  20108  cfilucfilOLD  20119  cfilucfil  20120  dscopn  20141  nmoi  20282  iccntr  20373  cphsqrcl2  20680  cmsss  20836  ivthlem3  20912  sca2rab  20970  ovolicc2lem3  20977  mdegleb  21510  aalioulem3  21775  ulm2  21825  ulmcn  21839  root1eq1  22168  atanlogsublem  22285  birthdaylem3  22322  logexprlim  22539  dchrisumlem3  22715  ax5seglem1  23125  ax5seglem2  23126  ax5seglem3a  23127  ax5seglem4  23129  ax5seglem9  23134  ax5seg  23135  axbtwnid  23136  axlowdimlem17  23155  axcontlem2  23162  axcontlem4  23164  axcontlem8  23168  constr3trllem2  23488  vdgrnn0pnf  23530  eupatrl  23540  grpoidinv  23646  gxadd  23713  rngosn3  23864  imsmetlem  24032  ipasslem1  24182  ip2eqi  24208  hvpncan  24392  pjid  25049  hmopre  25278  eigvalcl  25316  leopnmid  25493  superpos  25709  cvp  25730  ssct  25960  fnct  25964  xlt2addrd  26002  ordtconlem1  26306  fmcncfil  26313  esumfsup  26471  esumcvg  26487  insiga  26532  ballotlemirc  26866  signswch  26914  signstfvneq0  26925  signstfvcl  26926  subfacp1lem6  27025  prodeq2ii  27377  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  ftc1anclem5  28424  indexa  28580  sstotbnd3  28628  heiborlem6  28668  elpell1qr2  29166  oddcomabszz  29238  wepwsolem  29347  mendrng  29502  mendlmod  29503  hausgraph  29533  cncmpmax  29707  stoweidlem7  29755  stoweidlem34  29782  stoweidlem35  29783  stoweidlem49  29797  stoweidlem57  29805  stoweidlem59  29807  stoweidlem60  29808  stoweidlem62  29810  rusgranumwlks  30527  pgrple2abel  30719  atlatmstc  32804  atlatle  32805  glbconN  32861  intnatN  32891  lnnat  32911  atcvrj2b  32916  atexchcvrN  32924  llncvrlpln  33042  lplncvrlvol  33100  lautcvr  33576  trlatn0  33656  cdleme48fvg  33984  cdlemg33c  34192  dihcl  34755