Theorem sylancom 660

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 458	. 2 |- ( ( ph /\ ps ) -> ps )
3		sylancom.2	. 2 |- ( ( ch /\ ps ) -> th )
4	1, 2, 3	syl2anc 654	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  4736  sofld  5274  fimacnvdisj  5577  f1oexrnex  6516  wemoiso  6551  wemoiso2  6552  smorndom  6815  rdglim  6868  oaabs  7071  onomeneq  7488  domfi  7522  brwdom2  7776  infdiffi  7851  cantnflem1  7885  cantnflem1OLD  7908  wemapwe  7916  wemapweOLD  7917  cnfcom3lem  7924  cnfcom3lemOLD  7932  r1lim  7967  carduni  8139  ac5num  8194  infunsdom1  8370  cofsmo  8426  isf32lem6  8515  hsmexlem1  8583  ac6c4  8638  pwfseqlem1  8812  tskuni  8937  recgt1i  10216  avgle2  10552  uzindOLD  10723  rpnnen1lem1  10966  ioodisj  11401  fzneuz  11524  hasheni  12102  hashun2  12129  swrdccatin1  12357  reccn2  13057  isershft  13124  sumeq2ii  13153  demoivreALT  13467  xpnnenOLD  13474  bitsp1  13609  gcdneg  13692  eucalginv  13741  eucalg  13744  odzdvds  13849  fldivp1  13941  prmunb  13957  vdwap1  14020  setsid  14197  acsmapd  15330  cntzidss  15834  symggrp  15884  odmodnn0  16022  sylow2alem1  16095  dvdsrmul1  16678  dvrid  16713  znunit  17837  isphld  17924  frlmup1  18067  matunit  18325  cctop  18451  iscnp4  18708  iscncl  18714  cnntr  18720  tx2cn  19024  xkoco1cn  19071  qtopkgen  19124  hmeontr  19183  hmeores  19185  filssufilg  19325  ustuqtop1  19657  ustuqtop2  19658  utop2nei  19666  fmucndlem  19707  cfilufg  19709  metusttoOLD  19973  metustto  19974  cfilucfilOLD  19985  cfilucfil  19986  dscopn  20007  nmoi  20148  iccntr  20239  cphsqrcl2  20546  cmsss  20702  ivthlem3  20778  sca2rab  20836  ovolicc2lem3  20843  evl1val  21378  evl1sca  21380  pf1const  21396  mdegleb  21419  aalioulem3  21684  ulm2  21734  ulmcn  21748  root1eq1  22077  atanlogsublem  22194  birthdaylem3  22231  logexprlim  22448  dchrisumlem3  22624  ax5seglem1  22996  ax5seglem2  22997  ax5seglem3a  22998  ax5seglem4  23000  ax5seglem9  23005  ax5seg  23006  axbtwnid  23007  axlowdimlem17  23026  axcontlem2  23033  axcontlem4  23035  axcontlem8  23039  constr3trllem2  23359  vdgrnn0pnf  23401  eupatrl  23411  grpoidinv  23517  gxadd  23584  rngosn3  23735  imsmetlem  23903  ipasslem1  24053  ip2eqi  24079  hvpncan  24263  pjid  24920  hmopre  25149  eigvalcl  25187  leopnmid  25364  superpos  25580  cvp  25601  ssct  25832  fnct  25836  xlt2addrd  25875  ordtconlem1  26207  fmcncfil  26214  esumfsup  26372  esumcvg  26388  insiga  26433  ballotlemirc  26761  signswch  26809  signstfvneq0  26820  signstfvcl  26821  subfacp1lem6  26920  prodeq2ii  27272  ovoliunnfl  28274  voliunnfl  28276  volsupnfl  28277  ftc1anclem5  28312  indexa  28468  sstotbnd3  28516  heiborlem6  28556  elpell1qr2  29055  oddcomabszz  29127  wepwsolem  29236  mendrng  29391  mendlmod  29392  hausgraph  29422  cncmpmax  29596  stoweidlem7  29645  stoweidlem34  29672  stoweidlem35  29673  stoweidlem49  29687  stoweidlem57  29695  stoweidlem59  29697  stoweidlem60  29698  stoweidlem62  29700  rusgranumwlks  30417  pgrple2abel  30596  atlatmstc  32534  atlatle  32535  glbconN  32591  intnatN  32621  lnnat  32641  atcvrj2b  32646  atexchcvrN  32654  llncvrlpln  32772  lplncvrlvol  32830  lautcvr  33306  trlatn0  33386  cdleme48fvg  33714  cdlemg33c  33922  dihcl  34485