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  4109  tfrlem1  6552  tfrcl  6608  mkvprop  7462  ccfunen  7594  caucvgprprlemval  8019  suplocsrlem  8139  peano5uzti  9704  seqf1oglem2  10906  zfz1iso  11238  wrd2ind  11440  lcmneg  12796  prmind2  12842  pcfac  13073  cnmpt12  15278  cnmpt22  15285  limccnp2lem  15667  2sqlem6  16119  2sqlem8  16122  gropd  16168  grstructd2dom  16169  sbthom  16932