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  8136  initoeu2lem2  17984  mdetunilem9  22514  mdetuni0  22515  xmetrtri  24250  bl2in  24295  blhalf  24300  blssps  24319  blss  24320  blcld  24400  methaus  24415  metdstri  24747  metdscnlem  24751  metnrmlem3  24757  xlebnum  24871  pmltpclem1  25356  colinearalglem2  28841  axlowdim  28895  ssbnd  37789  totbndbnd  37790  heiborlem6  37817  2atm  39528  lplncvrlvol2  39616  dalem19  39683  paddasslem9  39829  pclclN  39892  pclfinN  39901  pclfinclN  39951  pexmidlem8N  39978  trlval3  40188  cdleme22b  40342  cdlemefr29bpre0N  40407  cdlemefr29clN  40408  cdlemefr32fvaN  40410  cdlemefr32fva1  40411  cdlemg31b0N  40695  cdlemg31b0a  40696  cdlemh  40818  dihmeetlem16N  41323  dihmeetlem18N  41325  dihmeetlem19N  41326  dihmeetlem20N  41327  hoidmvlelem1  46600