Theorem sylancom 420

Description: Syllogism inference with commutation of antecents. (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 110	. 2 |- ( ( ph /\ ps ) -> ps )
3		sylancom.2	. 2 |- ( ( ch /\ ps ) -> th )
4	1, 2, 3	syl2anc 411	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ordin  4511  fimacnvdisj  5556  fvimacnv  5798  ssct  7080  f1vrnfibi  7225  inl11  7369  ctssdc  7417  enomnilem  7442  enmkvlem  7465  djuen  7531  cauappcvgprlemlol  7978  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemlol  8001  caucvgprlemladdrl  8009  caucvgprprlemlol  8029  suplocsrlem  8139  recgt1i  9189  avgle2  9497  eluzmn  9878  xnn0le2is012  10218  ioodisj  10345  fzneuz  10457  zsupcllemstep  10611  fihashfn  11189  sseqn  11228  shftfvalg  11528  shftfval  11531  cvg1nlemres  11695  resqrexlem1arp  11715  maxabslemval  11918  xrmaxiflemval  11960  xrmaxadd  11971  xrminmax  11975  summodclem3  12091  fsumsplit  12118  mertenslemub  12245  fprodsplit  12308  demoivreALT  12485  bitsp1  12662  gcdneg  12703  bezoutlemsup  12730  eucalginv  12778  eucalg  12781  odzdvds  12968  pclemdc  13011  fldivp1  13071  prmunb  13085  ballotfilemirc  13219  enctlem  13267  ctiunctlemfo  13274  intopsn  13630  grpsubval  13801  mulgnndir  13904  gsumfzreidx  14090  gsumfzmptfidmadd  14092  gfsumval  14102  pwssnf1o  14153  znunit  14933  iscnp4  15209  cnntr  15216  tx2cn  15261  hmeontr  15304  hmeores  15306  xmetres2  15370  metres2  15372  limccnp2cntop  15668  limccoap  15669  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963