Theorem syl33anc 1387

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 1374	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  8133  initoeu2lem2  17977  mdetunilem9  22507  mdetuni0  22508  xmetrtri  24243  bl2in  24288  blhalf  24293  blssps  24312  blss  24313  blcld  24393  methaus  24408  metdstri  24740  metdscnlem  24744  metnrmlem3  24750  xlebnum  24864  pmltpclem1  25349  colinearalglem2  28834  axlowdim  28888  ssbnd  37782  totbndbnd  37783  heiborlem6  37810  2atm  39521  lplncvrlvol2  39609  dalem19  39676  paddasslem9  39822  pclclN  39885  pclfinN  39894  pclfinclN  39944  pexmidlem8N  39971  trlval3  40181  cdleme22b  40335  cdlemefr29bpre0N  40400  cdlemefr29clN  40401  cdlemefr32fvaN  40403  cdlemefr32fva1  40404  cdlemg31b0N  40688  cdlemg31b0a  40689  cdlemh  40811  dihmeetlem16N  41316  dihmeetlem18N  41318  dihmeetlem19N  41319  dihmeetlem20N  41320  hoidmvlelem1  46593