Theorem syl33anc 1413

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  xpord3inddlem  8198  initoeu2lem2  18219  mdetunilem9  22965  mdetuni0  22966  xmetrtri  24704  bl2in  24749  blhalf  24754  blssps  24773  blss  24774  blcld  24854  methaus  24869  metdstri  25201  metdscnlem  25205  metnrmlem3  25211  xlebnum  25316  pmltpclem1  25799  bdayfinbndlem1  28883  colinearalglem2  29515  axlowdim  29569  ssbnd  38914  totbndbnd  38915  heiborlem6  38942  2atm  40776  lplncvrlvol2  40864  dalem19  40931  paddasslem9  41077  pclclN  41140  pclfinN  41149  pclfinclN  41199  pexmidlem8N  41226  trlval3  41436  cdleme22b  41590  cdlemefr29bpre0N  41655  cdlemefr29clN  41656  cdlemefr32fvaN  41658  cdlemefr32fva1  41659  cdlemg31b0N  41943  cdlemg31b0a  41944  cdlemh  42066  dihmeetlem16N  42571  dihmeetlem18N  42573  dihmeetlem19N  42574  dihmeetlem20N  42575  hoidmvlelem1  47810  veroquadnolindfd  51265