Theorem sylancom 414

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 406	1 |- ( ( ph /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ordin  4267  fimacnvdisj  5265  fvimacnv  5489  ssct  6665  f1vrnfibi  6785  inl11  6902  ctssdc  6950  enomnilem  6960  djuen  7015  cauappcvgprlemlol  7403  cauappcvgprlemladdru  7412  cauappcvgprlemladdrl  7413  caucvgprlemlol  7426  caucvgprlemladdrl  7434  caucvgprprlemlol  7454  recgt1i  8566  avgle2  8865  xnn0le2is012  9542  ioodisj  9669  fzneuz  9774  fihashfn  10439  shftfvalg  10483  shftfval  10486  cvg1nlemres  10649  resqrexlem1arp  10669  maxabslemval  10872  xrmaxiflemval  10911  xrmaxadd  10922  xrminmax  10926  summodclem3  11041  fsumsplit  11068  mertenslemub  11195  demoivreALT  11330  zsupcllemstep  11486  gcdsupex  11494  gcdsupcl  11495  gcdneg  11518  bezoutlemsup  11543  eucalginv  11583  eucalg  11586  ctiunctlemfo  11795  iscnp4  12229  cnntr  12236  tx2cn  12281  xmetres2  12368  metres2  12370  limccnp2cntop  12602  isomninnlem  12917