Theorem syl33anc 1388

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  xpord3inddlem  8106  initoeu2lem2  17951  mdetunilem9  22576  mdetuni0  22577  xmetrtri  24311  bl2in  24356  blhalf  24361  blssps  24380  blss  24381  blcld  24461  methaus  24476  metdstri  24808  metdscnlem  24812  metnrmlem3  24818  xlebnum  24932  pmltpclem1  25417  bdayfinbndlem1  28475  colinearalglem2  28992  axlowdim  29046  ssbnd  38033  totbndbnd  38034  heiborlem6  38061  2atm  39897  lplncvrlvol2  39985  dalem19  40052  paddasslem9  40198  pclclN  40261  pclfinN  40270  pclfinclN  40320  pexmidlem8N  40347  trlval3  40557  cdleme22b  40711  cdlemefr29bpre0N  40776  cdlemefr29clN  40777  cdlemefr32fvaN  40779  cdlemefr32fva1  40780  cdlemg31b0N  41064  cdlemg31b0a  41065  cdlemh  41187  dihmeetlem16N  41692  dihmeetlem18N  41694  dihmeetlem19N  41695  dihmeetlem20N  41696  hoidmvlelem1  46947