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  8090  initoeu2lem2  17924  mdetunilem9  22536  mdetuni0  22537  xmetrtri  24271  bl2in  24316  blhalf  24321  blssps  24340  blss  24341  blcld  24421  methaus  24436  metdstri  24768  metdscnlem  24772  metnrmlem3  24778  xlebnum  24892  pmltpclem1  25377  colinearalglem2  28887  axlowdim  28941  ssbnd  37848  totbndbnd  37849  heiborlem6  37876  2atm  39646  lplncvrlvol2  39734  dalem19  39801  paddasslem9  39947  pclclN  40010  pclfinN  40019  pclfinclN  40069  pexmidlem8N  40096  trlval3  40306  cdleme22b  40460  cdlemefr29bpre0N  40525  cdlemefr29clN  40526  cdlemefr32fvaN  40528  cdlemefr32fva1  40529  cdlemg31b0N  40813  cdlemg31b0a  40814  cdlemh  40936  dihmeetlem16N  41441  dihmeetlem18N  41443  dihmeetlem19N  41444  dihmeetlem20N  41445  hoidmvlelem1  46717