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  1416  disjiun  4046  tfrlem1  6407  tfrcl  6463  mkvprop  7275  ccfunen  7396  caucvgprprlemval  7821  suplocsrlem  7941  peano5uzti  9501  seqf1oglem2  10687  zfz1iso  11008  wrd2ind  11199  lcmneg  12471  prmind2  12517  pcfac  12748  cnmpt12  14834  cnmpt22  14841  limccnp2lem  15223  2sqlem6  15672  2sqlem8  15675  gropd  15721  grstructd2dom  15722  sbthom  16106