Theorem sylancom 418

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ordin  4370  fimacnvdisj  5382  fvimacnv  5611  ssct  6796  f1vrnfibi  6922  inl11  7042  ctssdc  7090  enomnilem  7114  enmkvlem  7137  djuen  7188  cauappcvgprlemlol  7609  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  caucvgprlemlol  7632  caucvgprlemladdrl  7640  caucvgprprlemlol  7660  suplocsrlem  7770  recgt1i  8814  avgle2  9119  xnn0le2is012  9823  ioodisj  9950  fzneuz  10057  fihashfn  10735  shftfvalg  10782  shftfval  10785  cvg1nlemres  10949  resqrexlem1arp  10969  maxabslemval  11172  xrmaxiflemval  11213  xrmaxadd  11224  xrminmax  11228  summodclem3  11343  fsumsplit  11370  mertenslemub  11497  fprodsplit  11560  demoivreALT  11736  zsupcllemstep  11900  gcdsupex  11912  gcdsupcl  11913  gcdneg  11937  bezoutlemsup  11964  eucalginv  12010  eucalg  12013  odzdvds  12199  fldivp1  12300  prmunb  12314  enctlem  12387  ctiunctlemfo  12394  intopsn  12621  grpsubval  12749  iscnp4  13012  cnntr  13019  tx2cn  13064  hmeontr  13107  hmeores  13109  xmetres2  13173  metres2  13175  limccnp2cntop  13440  limccoap  13441  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084