Theorem syl6an 1478

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 316	. 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 104

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

This theorem is referenced by:  mapxpen  7034  prarloclem5  7720  ltsopr  7816  suplocsrlem  8028  nominpos  9382  ublbneg  9847  wrdsymb0  11150  ccats1pfxeqrex  11300  absle  11667  rexanre  11798  rexico  11799  climshftlemg  11880  serf0  11930  dvds1lem  12381  dvds2lem  12382  lmconst  14959  addcncntoplem  15304  bj-indind  16578