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  4078  tfrlem1  6460  tfrcl  6516  mkvprop  7336  ccfunen  7461  caucvgprprlemval  7886  suplocsrlem  8006  peano5uzti  9566  seqf1oglem2  10754  zfz1iso  11076  wrd2ind  11270  lcmneg  12611  prmind2  12657  pcfac  12888  cnmpt12  14976  cnmpt22  14983  limccnp2lem  15365  2sqlem6  15814  2sqlem8  15817  gropd  15863  grstructd2dom  15864  sbthom  16454