Theorem syl33anc 1341

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-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 )
syl33anc.7	|- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et /\ ze ) ) -> si )

Assertion

Ref	Expression
syl33anc	|- ( ph -> si )

Proof of Theorem syl33anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 |- ( ph -> ps )
2		syl12anc.2	. . 3 |- ( ph -> ch )
3		syl12anc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	3jca 1242	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		syl22anc.4	. 2 |- ( ph -> ta )
6		syl23anc.5	. 2 |- ( ph -> et )
7		syl33anc.6	. 2 |- ( ph -> ze )
8		syl33anc.7	. 2 |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et /\ ze ) ) -> si )
9	4, 5, 6, 7, 8	syl13anc 1328	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:  initoeu2lem2  16665  mdetunilem9  20426  mdetuni0  20427  xmetrtri  22160  bl2in  22205  blhalf  22210  blssps  22229  blss  22230  blcld  22310  methaus  22325  metdstri  22654  metdscnlem  22658  metnrmlem3  22664  xlebnum  22764  pmltpclem1  23217  colinearalglem2  25787  axlowdim  25841  ssbnd  33587  totbndbnd  33588  heiborlem6  33615  2atm  34813  lplncvrlvol2  34901  dalem19  34968  paddasslem9  35114  pclclN  35177  pclfinN  35186  pclfinclN  35236  pexmidlem8N  35263  trlval3  35474  cdleme22b  35629  cdlemefr29bpre0N  35694  cdlemefr29clN  35695  cdlemefr32fvaN  35697  cdlemefr32fva1  35698  cdlemg31b0N  35982  cdlemg31b0a  35983  cdlemh  36105  dihmeetlem16N  36611  dihmeetlem18N  36613  dihmeetlem19N  36614  dihmeetlem20N  36615  hoidmvlelem1  40809