Theorem syl33anc 1388

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 1129	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl33anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)
9	4, 5, 6, 7, 8	syl13anc 1375	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  xpord3inddlem  8108  initoeu2lem2  17953  mdetunilem9  22581  mdetuni0  22582  xmetrtri  24316  bl2in  24361  blhalf  24366  blssps  24385  blss  24386  blcld  24466  methaus  24481  metdstri  24813  metdscnlem  24817  metnrmlem3  24823  xlebnum  24937  pmltpclem1  25422  bdayfinbndlem1  28480  colinearalglem2  28998  axlowdim  29052  ssbnd  38068  totbndbnd  38069  heiborlem6  38096  2atm  39932  lplncvrlvol2  40020  dalem19  40087  paddasslem9  40233  pclclN  40296  pclfinN  40305  pclfinclN  40355  pexmidlem8N  40382  trlval3  40592  cdleme22b  40746  cdlemefr29bpre0N  40811  cdlemefr29clN  40812  cdlemefr32fvaN  40814  cdlemefr32fva1  40815  cdlemg31b0N  41099  cdlemg31b0a  41100  cdlemh  41222  dihmeetlem16N  41727  dihmeetlem18N  41729  dihmeetlem19N  41730  dihmeetlem20N  41731  hoidmvlelem1  46982