Theorem syl6an 1454

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  6960  prarloclem5  7633  ltsopr  7729  suplocsrlem  7941  nominpos  9295  ublbneg  9754  wrdsymb0  11048  ccats1pfxeqrex  11191  absle  11475  rexanre  11606  rexico  11607  climshftlemg  11688  serf0  11738  dvds1lem  12188  dvds2lem  12189  lmconst  14763  addcncntoplem  15108  bj-indind  16006