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  8155  initoeu2lem2  18170  mdetunilem9  22915  mdetuni0  22916  xmetrtri  24654  bl2in  24699  blhalf  24704  blssps  24723  blss  24724  blcld  24804  methaus  24819  metdstri  25151  metdscnlem  25155  metnrmlem3  25161  xlebnum  25266  pmltpclem1  25749  bdayfinbndlem1  28835  colinearalglem2  29467  axlowdim  29521  ssbnd  38690  totbndbnd  38691  heiborlem6  38718  2atm  40552  lplncvrlvol2  40640  dalem19  40707  paddasslem9  40853  pclclN  40916  pclfinN  40925  pclfinclN  40975  pexmidlem8N  41002  trlval3  41212  cdleme22b  41366  cdlemefr29bpre0N  41431  cdlemefr29clN  41432  cdlemefr32fvaN  41434  cdlemefr32fva1  41435  cdlemg31b0N  41719  cdlemg31b0a  41720  cdlemh  41842  dihmeetlem16N  42347  dihmeetlem18N  42349  dihmeetlem19N  42350  dihmeetlem20N  42351  hoidmvlelem1  47549  veroquadnolindfd  50929