Theorem sylcom 25

Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.)

Hypotheses

Ref	Expression
sylcom.1	|- ( ph -> ( ps -> ch ) )
sylcom.2	|- ( ps -> ( ch -> th ) )

Assertion

Ref	Expression
sylcom	|- ( ph -> ( ps -> th ) )

Proof of Theorem sylcom

Step	Hyp	Ref	Expression
1		sylcom.1	. 2 |- ( ph -> ( ps -> ch ) )
2		sylcom.2	. . 3 |- ( ps -> ( ch -> th ) )
3	2	a2i 11	. 2 |- ( ( ps -> ch ) -> ( ps -> th ) )
4	1, 3	syl 14	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl5com  26  syl6  29  syli  33  mpbidi  140  con4biddc  754  jaddc  761  con1biddc  770  necon4addc  2275  necon4bddc  2276  necon4ddc  2277  necon1addc  2281  necon1bddc  2282  dmcosseq  4603  iss  4654  funopg  4934  snon0  6356