Theorem syl3c 63

Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)

Hypotheses

Ref	Expression
syl3c.1	|- ( ph -> ps )
syl3c.2	|- ( ph -> ch )
syl3c.3	|- ( ph -> th )
syl3c.4	|- ( ps -> ( ch -> ( th -> ta ) ) )

Assertion

Ref	Expression
syl3c	|- ( ph -> ta )

Proof of Theorem syl3c

Step	Hyp	Ref	Expression
1		syl3c.3	. 2 |- ( ph -> th )
2		syl3c.1	. . 3 |- ( ph -> ps )
3		syl3c.2	. . 3 |- ( ph -> ch )
4		syl3c.4	. . 3 |- ( ps -> ( ch -> ( th -> ta ) ) )
5	2, 3, 4	sylc 62	. 2 |- ( ph -> ( th -> ta ) )
6	1, 5	mpd 13	1 |- ( ph -> ta )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  bilukdc  1441  disjiun  4088  tfrlem1  6517  tfrcl  6573  mkvprop  7400  ccfunen  7526  caucvgprprlemval  7951  suplocsrlem  8071  peano5uzti  9632  seqf1oglem2  10828  zfz1iso  11151  wrd2ind  11353  lcmneg  12709  prmind2  12755  pcfac  12986  cnmpt12  15081  cnmpt22  15088  limccnp2lem  15470  2sqlem6  15922  2sqlem8  15925  gropd  15971  grstructd2dom  15972  sbthom  16737