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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  bilukdc  1445  disjiun  4125  tfrlem1  6579  tfrcl  6635  mkvprop  7499  ccfunen  7631  caucvgprprlemval  8056  suplocsrlem  8176  peano5uzti  9759  seqf1oglem2  10972  zfz1iso  11309  wrd2ind  11511  lcmneg  12871  prmind2  12917  pcfac  13152  cnmpt12  15479  cnmpt22  15486  limccnp2lem  15868  2sqlem6  16405  2sqlem8  16408  gropd  16454  grstructd2dom  16455  sbthom  17237