Theorem syl33anc 1386

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

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

This theorem is referenced by:  xpord3inddlem  8161  initoeu2lem2  18032  mdetunilem9  22575  mdetuni0  22576  xmetrtri  24311  bl2in  24356  blhalf  24361  blssps  24380  blss  24381  blcld  24463  methaus  24478  metdstri  24810  metdscnlem  24814  metnrmlem3  24820  xlebnum  24934  pmltpclem1  25420  colinearalglem2  28853  axlowdim  28907  ssbnd  37770  totbndbnd  37771  heiborlem6  37798  2atm  39504  lplncvrlvol2  39592  dalem19  39659  paddasslem9  39805  pclclN  39868  pclfinN  39877  pclfinclN  39927  pexmidlem8N  39954  trlval3  40164  cdleme22b  40318  cdlemefr29bpre0N  40383  cdlemefr29clN  40384  cdlemefr32fvaN  40386  cdlemefr32fva1  40387  cdlemg31b0N  40671  cdlemg31b0a  40672  cdlemh  40794  dihmeetlem16N  41299  dihmeetlem18N  41301  dihmeetlem19N  41302  dihmeetlem20N  41303  hoidmvlelem1  46582