Theorem sylancom 397

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

Syntax hints:   -> wi 4   /\ wa 97

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

This theorem is referenced by:  ordin  4122  fimacnvdisj  5074  fvimacnv  5282  cauappcvgprlemlol  6745  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemlol  6768  caucvgprlemladdrl  6776  caucvgprprlemlol  6796  recgt1i  7864  avgle2  8166  ioodisj  8861  fzneuz  8963  shftfvalg  9419  shftfval  9422  cvg1nlemres  9584  resqrexlem1arp  9603