Theorem syl33anc 1510

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  initoeu2lem2  17017  mdetunilem9  20794  mdetuni0  20795  xmetrtri  22530  bl2in  22575  blhalf  22580  blssps  22599  blss  22600  blcld  22680  methaus  22695  metdstri  23024  metdscnlem  23028  metnrmlem3  23034  xlebnum  23134  pmltpclem1  23614  colinearalglem2  26206  axlowdim  26260  ssbnd  34129  totbndbnd  34130  heiborlem6  34157  2atm  35602  lplncvrlvol2  35690  dalem19  35757  paddasslem9  35903  pclclN  35966  pclfinN  35975  pclfinclN  36025  pexmidlem8N  36052  trlval3  36262  cdleme22b  36416  cdlemefr29bpre0N  36481  cdlemefr29clN  36482  cdlemefr32fvaN  36484  cdlemefr32fva1  36485  cdlemg31b0N  36769  cdlemg31b0a  36770  cdlemh  36892  dihmeetlem16N  37397  dihmeetlem18N  37399  dihmeetlem19N  37400  dihmeetlem20N  37401  hoidmvlelem1  41603