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  6584  tfrcl  6640  mkvprop  7504  ccfunen  7636  caucvgprprlemval  8061  suplocsrlem  8181  peano5uzti  9764  seqf1oglem2  10977  zfz1iso  11314  wrd2ind  11516  lcmneg  12876  prmind2  12922  pcfac  13157  cnmpt12  15530  cnmpt22  15537  limccnp2lem  15919  2sqlem6  16461  2sqlem8  16464  gropd  16510  grstructd2dom  16511  sbthom  17294