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  8158  initoeu2lem2  18033  mdetunilem9  22563  mdetuni0  22564  xmetrtri  24299  bl2in  24344  blhalf  24349  blssps  24368  blss  24369  blcld  24449  methaus  24464  metdstri  24796  metdscnlem  24800  metnrmlem3  24806  xlebnum  24920  pmltpclem1  25406  colinearalglem2  28891  axlowdim  28945  ssbnd  37817  totbndbnd  37818  heiborlem6  37845  2atm  39551  lplncvrlvol2  39639  dalem19  39706  paddasslem9  39852  pclclN  39915  pclfinN  39924  pclfinclN  39974  pexmidlem8N  40001  trlval3  40211  cdleme22b  40365  cdlemefr29bpre0N  40430  cdlemefr29clN  40431  cdlemefr32fvaN  40433  cdlemefr32fva1  40434  cdlemg31b0N  40718  cdlemg31b0a  40719  cdlemh  40841  dihmeetlem16N  41346  dihmeetlem18N  41348  dihmeetlem19N  41349  dihmeetlem20N  41350  hoidmvlelem1  46591