Theorem syl33anc 1333

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl33anc.7	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)

Assertion

Ref	Expression
syl33anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl33anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1235	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl33anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎)
9	4, 5, 6, 7, 8	syl13anc 1320	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  initoeu2lem2  16488  mdetunilem9  20245  mdetuni0  20246  xmetrtri  21970  bl2in  22015  blhalf  22020  blssps  22039  blss  22040  blcld  22120  methaus  22135  metdstri  22462  metdscnlem  22466  metnrmlem3  22472  xlebnum  22572  pmltpclem1  23024  colinearalglem2  25587  axlowdim  25641  ssbnd  32757  totbndbnd  32758  heiborlem6  32785  2atm  33831  lplncvrlvol2  33919  dalem19  33986  paddasslem9  34132  pclclN  34195  pclfinN  34204  pclfinclN  34254  pexmidlem8N  34281  trlval3  34492  cdleme22b  34647  cdlemefr29bpre0N  34712  cdlemefr29clN  34713  cdlemefr32fvaN  34715  cdlemefr32fva1  34716  cdlemg31b0N  35000  cdlemg31b0a  35001  cdlemh  35123  dihmeetlem16N  35629  dihmeetlem18N  35631  dihmeetlem19N  35632  dihmeetlem20N  35633  hoidmvlelem1  39485