Theorem syl33anc 1387

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 1374	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  8084  initoeu2lem2  17919  mdetunilem9  22533  mdetuni0  22534  xmetrtri  24268  bl2in  24313  blhalf  24318  blssps  24337  blss  24338  blcld  24418  methaus  24433  metdstri  24765  metdscnlem  24769  metnrmlem3  24775  xlebnum  24889  pmltpclem1  25374  colinearalglem2  28883  axlowdim  28937  ssbnd  37827  totbndbnd  37828  heiborlem6  37855  2atm  39565  lplncvrlvol2  39653  dalem19  39720  paddasslem9  39866  pclclN  39929  pclfinN  39938  pclfinclN  39988  pexmidlem8N  40015  trlval3  40225  cdleme22b  40379  cdlemefr29bpre0N  40444  cdlemefr29clN  40445  cdlemefr32fvaN  40447  cdlemefr32fva1  40448  cdlemg31b0N  40732  cdlemg31b0a  40733  cdlemh  40855  dihmeetlem16N  41360  dihmeetlem18N  41362  dihmeetlem19N  41363  dihmeetlem20N  41364  hoidmvlelem1  46632