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  1415  disjiun  4038  tfrlem1  6393  tfrcl  6449  mkvprop  7259  ccfunen  7375  caucvgprprlemval  7800  suplocsrlem  7920  peano5uzti  9480  seqf1oglem2  10663  zfz1iso  10984  lcmneg  12338  prmind2  12384  pcfac  12615  cnmpt12  14701  cnmpt22  14708  limccnp2lem  15090  2sqlem6  15539  2sqlem8  15542  gropd  15586  grstructd2dom  15587  sbthom  15898