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  4850  sofld  5387  fimacnvdisj  5690  f1oexrnex  6630  wemoiso  6665  wemoiso2  6666  smorndom  6932  rdglim  6985  oaabs  7186  onomeneq  7604  domfi  7638  brwdom2  7892  infdiffi  7967  cantnflem1  8001  cantnflem1OLD  8024  wemapwe  8032  wemapweOLD  8033  cnfcom3lem  8040  cnfcom3lemOLD  8048  r1lim  8083  carduni  8255  ac5num  8310  infunsdom1  8486  cofsmo  8542  isf32lem6  8631  hsmexlem1  8699  ac6c4  8754  pwfseqlem1  8929  tskuni  9054  recgt1i  10333  avgle2  10669  uzindOLD  10840  rpnnen1lem1  11083  ioodisj  11525  fzneuz  11651  hasheni  12229  hashun2  12257  swrdccatin1  12485  reccn2  13185  isershft  13252  sumeq2ii  13281  demoivreALT  13596  xpnnenOLD  13603  bitsp1  13738  gcdneg  13821  eucalginv  13870  eucalg  13873  odzdvds  13978  fldivp1  14070  prmunb  14086  vdwap1  14149  setsid  14326  acsmapd  15459  cntzidss  15966  symggrp  16016  odmodnn0  16156  sylow2alem1  16229  dvdsrmul1  16860  dvrid  16895  evl1val  17881  evl1sca  17886  pf1const  17898  znunit  18114  isphld  18201  frlmup1  18344  matunit  18609  cctop  18735  iscnp4  18992  iscncl  18998  cnntr  19004  tx2cn  19308  xkoco1cn  19355  qtopkgen  19408  hmeontr  19467  hmeores  19469  filssufilg  19609  ustuqtop1  19941  ustuqtop2  19942  utop2nei  19950  fmucndlem  19991  cfilufg  19993  metusttoOLD  20257  metustto  20258  cfilucfilOLD  20269  cfilucfil  20270  dscopn  20291  nmoi  20432  iccntr  20523  cphsqrcl2  20830  cmsss  20986  ivthlem3  21062  sca2rab  21120  ovolicc2lem3  21127  mdegleb  21661  aalioulem3  21926  ulm2  21976  ulmcn  21990  root1eq1  22319  atanlogsublem  22436  birthdaylem3  22473  logexprlim  22690  dchrisumlem3  22866  ax5seglem1  23319  ax5seglem2  23320  ax5seglem3a  23321  ax5seglem4  23323  ax5seglem9  23328  ax5seg  23329  axbtwnid  23330  axlowdimlem17  23349  axcontlem2  23356  axcontlem4  23358  axcontlem8  23362  constr3trllem2  23682  vdgrnn0pnf  23724  eupatrl  23734  grpoidinv  23840  gxadd  23907  rngosn3  24058  imsmetlem  24226  ipasslem1  24376  ip2eqi  24402  hvpncan  24586  pjid  25243  hmopre  25472  eigvalcl  25510  leopnmid  25687  superpos  25903  cvp  25924  ssct  26153  fnct  26157  xlt2addrd  26195  ordtconlem1  26492  fmcncfil  26499  esumfsup  26657  esumcvg  26673  insiga  26718  ballotlemirc  27051  signswch  27099  signstfvneq0  27110  signstfvcl  27111  subfacp1lem6  27210  prodeq2ii  27563  ovoliunnfl  28574  voliunnfl  28576  volsupnfl  28577  ftc1anclem5  28612  indexa  28768  sstotbnd3  28816  heiborlem6  28856  elpell1qr2  29354  oddcomabszz  29426  wepwsolem  29535  mendrng  29690  mendlmod  29691  hausgraph  29721  cncmpmax  29895  stoweidlem7  29943  stoweidlem34  29970  stoweidlem35  29971  stoweidlem49  29985  stoweidlem57  29993  stoweidlem59  29995  stoweidlem60  29996  stoweidlem62  29998  rusgranumwlks  30715  pgrple2abel  30911  telescfzgsum  30954  atlatmstc  33273  atlatle  33274  glbconN  33330  intnatN  33360  lnnat  33380  atcvrj2b  33385  atexchcvrN  33393  llncvrlpln  33511  lplncvrlvol  33569  lautcvr  34045  trlatn0  34125  cdleme48fvg  34453  cdlemg33c  34661  dihcl  35224