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  1445  disjiun  4120  tfrlem1  6569  tfrcl  6625  mkvprop  7488  ccfunen  7620  caucvgprprlemval  8045  suplocsrlem  8165  peano5uzti  9733  seqf1oglem2  10935  zfz1iso  11271  wrd2ind  11473  lcmneg  12830  prmind2  12876  pcfac  13107  cnmpt12  15311  cnmpt22  15318  limccnp2lem  15700  2sqlem6  16153  2sqlem8  16156  gropd  16202  grstructd2dom  16203  sbthom  16976