Theorem syl6an 1422

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  6814  prarloclem5  7441  ltsopr  7537  suplocsrlem  7749  nominpos  9094  ublbneg  9551  absle  11031  rexanre  11162  rexico  11163  climshftlemg  11243  serf0  11293  dvds1lem  11742  dvds2lem  11743  lmconst  12856  addcncntoplem  13191  bj-indind  13814