Theorem syl33anc 1384

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 1127	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl33anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)
9	4, 5, 6, 7, 8	syl13anc 1371	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  xpord3inddlem  8178  initoeu2lem2  18069  mdetunilem9  22642  mdetuni0  22643  xmetrtri  24381  bl2in  24426  blhalf  24431  blssps  24450  blss  24451  blcld  24534  methaus  24549  metdstri  24887  metdscnlem  24891  metnrmlem3  24897  xlebnum  25011  pmltpclem1  25497  colinearalglem2  28937  axlowdim  28991  ssbnd  37775  totbndbnd  37776  heiborlem6  37803  2atm  39510  lplncvrlvol2  39598  dalem19  39665  paddasslem9  39811  pclclN  39874  pclfinN  39883  pclfinclN  39933  pexmidlem8N  39960  trlval3  40170  cdleme22b  40324  cdlemefr29bpre0N  40389  cdlemefr29clN  40390  cdlemefr32fvaN  40392  cdlemefr32fva1  40393  cdlemg31b0N  40677  cdlemg31b0a  40678  cdlemh  40800  dihmeetlem16N  41305  dihmeetlem18N  41307  dihmeetlem19N  41308  dihmeetlem20N  41309  hoidmvlelem1  46551