Theorem sylancom 411

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  ordin  4142  fimacnvdisj  5099  fvimacnv  5308  f1vrnfibi  6443  cauappcvgprlemlol  6888  cauappcvgprlemladdru  6897  cauappcvgprlemladdrl  6898  caucvgprlemlol  6911  caucvgprlemladdrl  6919  caucvgprprlemlol  6939  recgt1i  8032  avgle2  8328  ioodisj  9080  fzneuz  9183  sizefn  9813  shftfvalg  9833  shftfval  9836  cvg1nlemres  9998  resqrexlem1arp  10018  maxabslemval  10221  zsupcllemstep  10474  gcdsupex  10482  gcdsupcl  10483  gcdneg  10506  bezoutlemsup  10531  eucalginv  10571  eucialg  10574