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  4104  tfrlem1  6539  tfrcl  6595  mkvprop  7449  ccfunen  7578  caucvgprprlemval  8003  suplocsrlem  8123  peano5uzti  9686  seqf1oglem2  10882  zfz1iso  11213  wrd2ind  11415  lcmneg  12771  prmind2  12817  pcfac  13048  cnmpt12  15152  cnmpt22  15159  limccnp2lem  15541  2sqlem6  15993  2sqlem8  15996  gropd  16042  grstructd2dom  16043  sbthom  16806