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  4432  fimacnvdisj  5460  fvimacnv  5695  ssct  6913  f1vrnfibi  7047  inl11  7167  ctssdc  7215  enomnilem  7240  enmkvlem  7263  djuen  7323  cauappcvgprlemlol  7760  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemlol  7783  caucvgprlemladdrl  7791  caucvgprprlemlol  7811  suplocsrlem  7921  recgt1i  8971  avgle2  9279  xnn0le2is012  9988  ioodisj  10115  fzneuz  10223  zsupcllemstep  10372  fihashfn  10945  shftfvalg  11129  shftfval  11132  cvg1nlemres  11296  resqrexlem1arp  11316  maxabslemval  11519  xrmaxiflemval  11561  xrmaxadd  11572  xrminmax  11576  summodclem3  11691  fsumsplit  11718  mertenslemub  11845  fprodsplit  11908  demoivreALT  12085  bitsp1  12262  gcdneg  12303  bezoutlemsup  12330  eucalginv  12378  eucalg  12381  odzdvds  12568  pclemdc  12611  fldivp1  12671  prmunb  12685  enctlem  12803  ctiunctlemfo  12810  pwssnf1o  13130  intopsn  13199  grpsubval  13378  mulgnndir  13487  gsumfzreidx  13673  gsumfzmptfidmadd  13675  znunit  14421  iscnp4  14690  cnntr  14697  tx2cn  14742  hmeontr  14785  hmeores  14787  xmetres2  14851  metres2  14853  limccnp2cntop  15149  limccoap  15150  isomninnlem  15969  iswomninnlem  15988  ismkvnnlem  15991