Theorem syl33anc 1381

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  initoeu2lem2  17278  mdetunilem9  21232  mdetuni0  21233  xmetrtri  22968  bl2in  23013  blhalf  23018  blssps  23037  blss  23038  blcld  23118  methaus  23133  metdstri  23462  metdscnlem  23466  metnrmlem3  23472  xlebnum  23572  pmltpclem1  24052  colinearalglem2  26696  axlowdim  26750  ssbnd  35070  totbndbnd  35071  heiborlem6  35098  2atm  36667  lplncvrlvol2  36755  dalem19  36822  paddasslem9  36968  pclclN  37031  pclfinN  37040  pclfinclN  37090  pexmidlem8N  37117  trlval3  37327  cdleme22b  37481  cdlemefr29bpre0N  37546  cdlemefr29clN  37547  cdlemefr32fvaN  37549  cdlemefr32fva1  37550  cdlemg31b0N  37834  cdlemg31b0a  37835  cdlemh  37957  dihmeetlem16N  38462  dihmeetlem18N  38464  dihmeetlem19N  38465  dihmeetlem20N  38466  hoidmvlelem1  42884