Theorem syl33anc 1385

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

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl33anc.7	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)

Assertion

Ref	Expression
syl33anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl33anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1128	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl33anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)
9	4, 5, 6, 7, 8	syl13anc 1372	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  xpord3inddlem  8142  initoeu2lem2  17967  mdetunilem9  22129  mdetuni0  22130  xmetrtri  23868  bl2in  23913  blhalf  23918  blssps  23937  blss  23938  blcld  24021  methaus  24036  metdstri  24374  metdscnlem  24378  metnrmlem3  24384  xlebnum  24488  pmltpclem1  24972  colinearalglem2  28203  axlowdim  28257  ssbnd  36742  totbndbnd  36743  heiborlem6  36770  2atm  38484  lplncvrlvol2  38572  dalem19  38639  paddasslem9  38785  pclclN  38848  pclfinN  38857  pclfinclN  38907  pexmidlem8N  38934  trlval3  39144  cdleme22b  39298  cdlemefr29bpre0N  39363  cdlemefr29clN  39364  cdlemefr32fvaN  39366  cdlemefr32fva1  39367  cdlemg31b0N  39651  cdlemg31b0a  39652  cdlemh  39774  dihmeetlem16N  40279  dihmeetlem18N  40281  dihmeetlem19N  40282  dihmeetlem20N  40283  hoidmvlelem1  45390