Theorem syl33anc 1382

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

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

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  xpord3inddlem  8134  initoeu2lem2  17967  mdetunilem9  22444  mdetuni0  22445  xmetrtri  24183  bl2in  24228  blhalf  24233  blssps  24252  blss  24253  blcld  24336  methaus  24351  metdstri  24689  metdscnlem  24693  metnrmlem3  24699  xlebnum  24813  pmltpclem1  25299  colinearalglem2  28634  axlowdim  28688  ssbnd  37146  totbndbnd  37147  heiborlem6  37174  2atm  38888  lplncvrlvol2  38976  dalem19  39043  paddasslem9  39189  pclclN  39252  pclfinN  39261  pclfinclN  39311  pexmidlem8N  39338  trlval3  39548  cdleme22b  39702  cdlemefr29bpre0N  39767  cdlemefr29clN  39768  cdlemefr32fvaN  39770  cdlemefr32fva1  39771  cdlemg31b0N  40055  cdlemg31b0a  40056  cdlemh  40178  dihmeetlem16N  40683  dihmeetlem18N  40685  dihmeetlem19N  40686  dihmeetlem20N  40687  hoidmvlelem1  45796