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  8156  initoeu2lem2  18110  mdetunilem9  22848  mdetuni0  22849  xmetrtri  24587  bl2in  24632  blhalf  24637  blssps  24656  blss  24657  blcld  24737  methaus  24752  metdstri  25084  metdscnlem  25088  metnrmlem3  25094  xlebnum  25199  pmltpclem1  25682  bdayfinbndlem1  28740  colinearalglem2  29372  axlowdim  29426  ssbnd  38546  totbndbnd  38547  heiborlem6  38574  2atm  40408  lplncvrlvol2  40496  dalem19  40563  paddasslem9  40709  pclclN  40772  pclfinN  40781  pclfinclN  40831  pexmidlem8N  40858  trlval3  41068  cdleme22b  41222  cdlemefr29bpre0N  41287  cdlemefr29clN  41288  cdlemefr32fvaN  41290  cdlemefr32fva1  41291  cdlemg31b0N  41575  cdlemg31b0a  41576  cdlemh  41698  dihmeetlem16N  42203  dihmeetlem18N  42205  dihmeetlem19N  42206  dihmeetlem20N  42207  hoidmvlelem1  47431  veroquadnolindfd  50826