Theorem syl321anc 1348

Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.4	|- ( ph -> ta )
syl23anc.5	|- ( ph -> et )
syl33anc.6	|- ( ph -> ze )
syl321anc.7	|- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) /\ ze ) -> si )

Assertion

Ref	Expression
syl321anc	|- ( ph -> si )

Proof of Theorem syl321anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 |- ( ph -> ps )
2		syl12anc.2	. 2 |- ( ph -> ch )
3		syl12anc.3	. 2 |- ( ph -> th )
4		syl22anc.4	. . 3 |- ( ph -> ta )
5		syl23anc.5	. . 3 |- ( ph -> et )
6	4, 5	jca 554	. 2 |- ( ph -> ( ta /\ et ) )
7		syl33anc.6	. 2 |- ( ph -> ze )
8		syl321anc.7	. 2 |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) /\ ze ) -> si )
9	1, 2, 3, 6, 7, 8	syl311anc 1340	1 |- ( ph -> si )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl322anc  1354  cxple2ad  24471  chordthmlem3  24561  nosupbnd1lem3  31856  nosupbnd1lem4  31857  4noncolr2  34740  4noncolr1  34741  3atlem5  34773  2lplnj  34906  llnmod2i2  35149  dalawlem11  35167  dalawlem12  35168  cdleme43dN  35780  cdleme4gfv  35795  cdlemeg46nlpq  35805  cdlemg17bq  35961  cdlemg31b0N  35982  cdlemg31b0a  35983  cdlemg31c  35987  cdlemg39  36004  cdlemk47  36237  lincext3  42245