Theorem syl33anc 1412

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

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

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 1105

This theorem is referenced by:  xpord3inddlem  8151  initoeu2lem2  18073  mdetunilem9  22758  mdetuni0  22759  xmetrtri  24493  bl2in  24538  blhalf  24543  blssps  24562  blss  24563  blcld  24643  methaus  24658  metdstri  24990  metdscnlem  24994  metnrmlem3  25000  xlebnum  25105  pmltpclem1  25588  bdayfinbndlem1  28638  colinearalglem2  29235  axlowdim  29289  ssbnd  38417  totbndbnd  38418  heiborlem6  38445  2atm  40279  lplncvrlvol2  40367  dalem19  40434  paddasslem9  40580  pclclN  40643  pclfinN  40652  pclfinclN  40702  pexmidlem8N  40729  trlval3  40939  cdleme22b  41093  cdlemefr29bpre0N  41158  cdlemefr29clN  41159  cdlemefr32fvaN  41161  cdlemefr32fva1  41162  cdlemg31b0N  41446  cdlemg31b0a  41447  cdlemh  41569  dihmeetlem16N  42074  dihmeetlem18N  42076  dihmeetlem19N  42077  dihmeetlem20N  42078  hoidmvlelem1  47289