Theorem syl33anc 1408

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  xpord3inddlem  8138  initoeu2lem2  18062  mdetunilem9  22738  mdetuni0  22739  xmetrtri  24473  bl2in  24518  blhalf  24523  blssps  24542  blss  24543  blcld  24623  methaus  24638  metdstri  24970  metdscnlem  24974  metnrmlem3  24980  xlebnum  25085  pmltpclem1  25568  bdayfinbndlem1  28618  colinearalglem2  29166  axlowdim  29220  ssbnd  38299  totbndbnd  38300  heiborlem6  38327  2atm  40163  lplncvrlvol2  40251  dalem19  40318  paddasslem9  40464  pclclN  40527  pclfinN  40536  pclfinclN  40586  pexmidlem8N  40613  trlval3  40823  cdleme22b  40977  cdlemefr29bpre0N  41042  cdlemefr29clN  41043  cdlemefr32fvaN  41045  cdlemefr32fva1  41046  cdlemg31b0N  41330  cdlemg31b0a  41331  cdlemh  41453  dihmeetlem16N  41958  dihmeetlem18N  41960  dihmeetlem19N  41961  dihmeetlem20N  41962  hoidmvlelem1  47167