Theorem sylancom 649

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  ordin  4571  sofld  5277  fimacnvdisj  5580  wemoiso  6037  wemoiso2  6038  smorndom  6589  rdglim  6643  oaabs  6846  onomeneq  7255  domfi  7289  brwdom2  7497  infdiffi  7568  cantnflem1  7601  wemapwe  7610  cnfcom3lem  7616  r1lim  7654  carduni  7824  ac5num  7873  infunsdom1  8049  cofsmo  8105  isf32lem6  8194  hsmexlem1  8262  ac6c4  8317  pwfseqlem1  8489  tskuni  8614  recgt1i  9863  avgle2  10164  uzindOLD  10320  rpnnen1lem1  10556  ioodisj  10982  fzneuz  11083  hasheni  11587  hashun2  11612  reccn2  12345  isershft  12412  sumeq2ii  12442  demoivreALT  12757  xpnnenOLD  12764  bitsp1  12898  gcdneg  12981  eucalginv  13030  eucalg  13033  odzdvds  13136  fldivp1  13221  prmunb  13237  vdwap1  13300  setsid  13463  acsmapd  14559  symggrp  15058  cntzidss  15091  odmodnn0  15133  sylow2alem1  15206  dvdsrmul1  15713  dvrid  15748  znunit  16799  isphld  16840  cctop  17025  iscnp4  17281  iscncl  17287  cnntr  17293  tx2cn  17595  xkoco1cn  17642  qtopkgen  17695  hmeontr  17754  hmeores  17756  filssufilg  17896  ustuqtop1  18224  ustuqtop2  18225  utop2nei  18233  fmucndlem  18274  cfilufg  18276  metusttoOLD  18540  metustto  18541  cfilucfilOLD  18552  cfilucfil  18553  dscopn  18574  nmoi  18715  iccntr  18805  cphsqrcl2  19102  cmsss  19256  ivthlem3  19303  sca2rab  19361  ovolicc2lem3  19368  evl1val  19901  evl1sca  19903  pf1const  19919  mdegleb  19940  aalioulem3  20204  ulm2  20254  ulmcn  20268  root1eq1  20592  atanlogsublem  20708  birthdaylem3  20745  logexprlim  20962  dchrisumlem3  21138  constr3trllem2  21591  vdgrnn0pnf  21633  eupatrl  21643  grpoidinv  21749  gxadd  21816  rngosn3  21967  imsmetlem  22135  ipasslem1  22285  ip2eqi  22311  hvpncan  22494  pjid  23150  hmopre  23379  eigvalcl  23417  leopnmid  23594  superpos  23810  cvp  23831  ssct  24054  fnct  24058  xlt2addrd  24077  fmcncfil  24270  esumfsup  24413  esumcvg  24429  insiga  24473  ballotlemirc  24742  subfacp1lem6  24824  prodeq2ii  25192  ax5seglem1  25771  ax5seglem2  25772  ax5seglem3a  25773  ax5seglem4  25775  ax5seglem9  25780  ax5seg  25781  axbtwnid  25782  axlowdimlem17  25801  axcontlem2  25808  axcontlem4  25810  axcontlem8  25814  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  indexa  26325  sstotbnd3  26375  heiborlem6  26415  elpell1qr2  26825  oddcomabszz  26897  wepwsolem  27006  mendrng  27368  mendlmod  27369  hausgraph  27399  cncmpmax  27570  stoweidlem7  27623  stoweidlem34  27650  stoweidlem35  27651  stoweidlem49  27665  stoweidlem57  27673  stoweidlem59  27675  stoweidlem60  27676  stoweidlem62  27678  ubmelm1fzo  27987  swrdccatin1  28016  atlatmstc  29802  atlatle  29803  glbconN  29859  intnatN  29889  lnnat  29909  atcvrj2b  29914  atexchcvrN  29922  llncvrlpln  30040  lplncvrlvol  30098  lautcvr  30574  trlatn0  30654  cdleme48fvg  30982  cdlemg33c  31190  dihcl  31753

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361