Theorem sylc 56

Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)

Hypotheses

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

Assertion

Ref	Expression
sylc	|- (ph -> th)

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.1	. . 3 |- (ph -> ps)
2		sylc.2	. . 3 |- (ph -> ch)
3		sylc.3	. . 3 |- (ps -> (ch -> th))
4	1, 2, 3	syl2im 34	. 2 |- (ph -> (ph -> th))
5	4	pm2.43i 43	1 |- (ph -> th)

Syntax hints:   -> wi 4

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

This theorem is referenced by:  syl3c  57  mpsyl  59  jc  139  2thd  231  jca  518  syl2anc  642  nfimd  1808  ax12  1935  ax12from12o  2156  equid1  2158  elex22  2871  elex2  2872  spcimdv  2937  spsbcd  3060  nnceleq  4431  tfinltfin  4502  sfinltfin  4536  sfin111  4537  phialllem1  4617  fvopab4t  5386  fvelrn  5414  frd  5923  refd  5928  enadjlem1  6060  enadj  6061  enprmaplem3  6079  1cnc  6140