Theorem syl33anc 1384

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  initoeu2lem2  17730  mdetunilem9  21769  mdetuni0  21770  xmetrtri  23508  bl2in  23553  blhalf  23558  blssps  23577  blss  23578  blcld  23661  methaus  23676  metdstri  24014  metdscnlem  24018  metnrmlem3  24024  xlebnum  24128  pmltpclem1  24612  colinearalglem2  27275  axlowdim  27329  ssbnd  35946  totbndbnd  35947  heiborlem6  35974  2atm  37541  lplncvrlvol2  37629  dalem19  37696  paddasslem9  37842  pclclN  37905  pclfinN  37914  pclfinclN  37964  pexmidlem8N  37991  trlval3  38201  cdleme22b  38355  cdlemefr29bpre0N  38420  cdlemefr29clN  38421  cdlemefr32fvaN  38423  cdlemefr32fva1  38424  cdlemg31b0N  38708  cdlemg31b0a  38709  cdlemh  38831  dihmeetlem16N  39336  dihmeetlem18N  39338  dihmeetlem19N  39339  dihmeetlem20N  39340  hoidmvlelem1  44133