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  1440  disjiun  4083  tfrlem1  6473  tfrcl  6529  mkvprop  7356  ccfunen  7482  caucvgprprlemval  7907  suplocsrlem  8027  peano5uzti  9587  seqf1oglem2  10781  zfz1iso  11104  wrd2ind  11303  lcmneg  12645  prmind2  12691  pcfac  12922  cnmpt12  15010  cnmpt22  15017  limccnp2lem  15399  2sqlem6  15848  2sqlem8  15851  gropd  15897  grstructd2dom  15898  sbthom  16630