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  7033  prarloclem5  7719  ltsopr  7815  suplocsrlem  8027  nominpos  9381  ublbneg  9846  wrdsymb0  11145  ccats1pfxeqrex  11295  absle  11649  rexanre  11780  rexico  11781  climshftlemg  11862  serf0  11912  dvds1lem  12362  dvds2lem  12363  lmconst  14939  addcncntoplem  15284  bj-indind  16527