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  17275  mdetunilem9  21229  mdetuni0  21230  xmetrtri  22965  bl2in  23010  blhalf  23015  blssps  23034  blss  23035  blcld  23115  methaus  23130  metdstri  23459  metdscnlem  23463  metnrmlem3  23469  xlebnum  23569  pmltpclem1  24049  colinearalglem2  26693  axlowdim  26747  ssbnd  35081  totbndbnd  35082  heiborlem6  35109  2atm  36678  lplncvrlvol2  36766  dalem19  36833  paddasslem9  36979  pclclN  37042  pclfinN  37051  pclfinclN  37101  pexmidlem8N  37128  trlval3  37338  cdleme22b  37492  cdlemefr29bpre0N  37557  cdlemefr29clN  37558  cdlemefr32fvaN  37560  cdlemefr32fva1  37561  cdlemg31b0N  37845  cdlemg31b0a  37846  cdlemh  37968  dihmeetlem16N  38473  dihmeetlem18N  38475  dihmeetlem19N  38476  dihmeetlem20N  38477  hoidmvlelem1  42926