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  6474  tfrcl  6530  mkvprop  7357  ccfunen  7483  caucvgprprlemval  7908  suplocsrlem  8028  peano5uzti  9588  seqf1oglem2  10783  zfz1iso  11106  wrd2ind  11308  lcmneg  12664  prmind2  12710  pcfac  12941  cnmpt12  15030  cnmpt22  15037  limccnp2lem  15419  2sqlem6  15868  2sqlem8  15871  gropd  15917  grstructd2dom  15918  sbthom  16681