Theorem syl33anc 1412

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 1399	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  8159  initoeu2lem2  18097  mdetunilem9  22814  mdetuni0  22815  xmetrtri  24549  bl2in  24594  blhalf  24599  blssps  24618  blss  24619  blcld  24699  methaus  24714  metdstri  25046  metdscnlem  25050  metnrmlem3  25056  xlebnum  25161  pmltpclem1  25644  bdayfinbndlem1  28697  colinearalglem2  29294  axlowdim  29348  ssbnd  38480  totbndbnd  38481  heiborlem6  38508  2atm  40342  lplncvrlvol2  40430  dalem19  40497  paddasslem9  40643  pclclN  40706  pclfinN  40715  pclfinclN  40765  pexmidlem8N  40792  trlval3  41002  cdleme22b  41156  cdlemefr29bpre0N  41221  cdlemefr29clN  41222  cdlemefr32fvaN  41224  cdlemefr32fva1  41225  cdlemg31b0N  41509  cdlemg31b0a  41510  cdlemh  41632  dihmeetlem16N  42137  dihmeetlem18N  42139  dihmeetlem19N  42140  dihmeetlem20N  42141  hoidmvlelem1  47350