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  1438  disjiun  4081  tfrlem1  6469  tfrcl  6525  mkvprop  7348  ccfunen  7473  caucvgprprlemval  7898  suplocsrlem  8018  peano5uzti  9578  seqf1oglem2  10772  zfz1iso  11095  wrd2ind  11294  lcmneg  12636  prmind2  12682  pcfac  12913  cnmpt12  15001  cnmpt22  15008  limccnp2lem  15390  2sqlem6  15839  2sqlem8  15842  gropd  15888  grstructd2dom  15889  sbthom  16566