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  1438  disjiun  4077  tfrlem1  6452  tfrcl  6508  mkvprop  7321  ccfunen  7446  caucvgprprlemval  7871  suplocsrlem  7991  peano5uzti  9551  seqf1oglem2  10737  zfz1iso  11058  wrd2ind  11250  lcmneg  12591  prmind2  12637  pcfac  12868  cnmpt12  14955  cnmpt22  14962  limccnp2lem  15344  2sqlem6  15793  2sqlem8  15796  gropd  15842  grstructd2dom  15843  sbthom  16353