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  8096  initoeu2lem2  17939  mdetunilem9  22564  mdetuni0  22565  xmetrtri  24299  bl2in  24344  blhalf  24349  blssps  24368  blss  24369  blcld  24449  methaus  24464  metdstri  24796  metdscnlem  24800  metnrmlem3  24806  xlebnum  24920  pmltpclem1  25405  bdayfinbndlem1  28463  colinearalglem2  28980  axlowdim  29034  ssbnd  37985  totbndbnd  37986  heiborlem6  38013  2atm  39783  lplncvrlvol2  39871  dalem19  39938  paddasslem9  40084  pclclN  40147  pclfinN  40156  pclfinclN  40206  pexmidlem8N  40233  trlval3  40443  cdleme22b  40597  cdlemefr29bpre0N  40662  cdlemefr29clN  40663  cdlemefr32fvaN  40665  cdlemefr32fva1  40666  cdlemg31b0N  40950  cdlemg31b0a  40951  cdlemh  41073  dihmeetlem16N  41578  dihmeetlem18N  41580  dihmeetlem19N  41581  dihmeetlem20N  41582  hoidmvlelem1  46835