Theorem syl6an 1414

Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)

Hypotheses

Ref	Expression
syl6an.1	|- ( ph -> ps )
syl6an.2	|- ( ph -> ( ch -> th ) )
syl6an.3	|- ( ( ps /\ th ) -> ta )

Assertion

Ref	Expression
syl6an	|- ( ph -> ( ch -> ta ) )

Proof of Theorem syl6an

Step	Hyp	Ref	Expression
1		syl6an.2	. . 3 |- ( ph -> ( ch -> th ) )
2		syl6an.1	. . 3 |- ( ph -> ps )
3	1, 2	jctild 314	. 2 |- ( ph -> ( ch -> ( ps /\ th ) ) )
4		syl6an.3	. 2 |- ( ( ps /\ th ) -> ta )
5	3, 4	syl6 33	1 |- ( ph -> ( ch -> ta ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mapxpen  6793  prarloclem5  7420  ltsopr  7516  suplocsrlem  7728  nominpos  9070  ublbneg  9522  absle  10989  rexanre  11120  rexico  11121  climshftlemg  11199  serf0  11249  dvds1lem  11698  dvds2lem  11699  lmconst  12627  addcncntoplem  12962  bj-indind  13518