Theorem syl33anc 1386

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 1373	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  8180  initoeu2lem2  18061  mdetunilem9  22627  mdetuni0  22628  xmetrtri  24366  bl2in  24411  blhalf  24416  blssps  24435  blss  24436  blcld  24519  methaus  24534  metdstri  24874  metdscnlem  24878  metnrmlem3  24884  xlebnum  24998  pmltpclem1  25484  colinearalglem2  28923  axlowdim  28977  ssbnd  37796  totbndbnd  37797  heiborlem6  37824  2atm  39530  lplncvrlvol2  39618  dalem19  39685  paddasslem9  39831  pclclN  39894  pclfinN  39903  pclfinclN  39953  pexmidlem8N  39980  trlval3  40190  cdleme22b  40344  cdlemefr29bpre0N  40409  cdlemefr29clN  40410  cdlemefr32fvaN  40412  cdlemefr32fva1  40413  cdlemg31b0N  40697  cdlemg31b0a  40698  cdlemh  40820  dihmeetlem16N  41325  dihmeetlem18N  41327  dihmeetlem19N  41328  dihmeetlem20N  41329  hoidmvlelem1  46615