Theorem syl33anc 1393

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  xpord3inddlem  8101  initoeu2lem2  17980  mdetunilem9  22610  mdetuni0  22611  xmetrtri  24345  bl2in  24390  blhalf  24395  blssps  24414  blss  24415  blcld  24495  methaus  24510  metdstri  24842  metdscnlem  24846  metnrmlem3  24852  xlebnum  24957  pmltpclem1  25440  bdayfinbndlem1  28484  colinearalglem2  29001  axlowdim  29055  ssbnd  38162  totbndbnd  38163  heiborlem6  38190  2atm  40026  lplncvrlvol2  40114  dalem19  40181  paddasslem9  40327  pclclN  40390  pclfinN  40399  pclfinclN  40449  pexmidlem8N  40476  trlval3  40686  cdleme22b  40840  cdlemefr29bpre0N  40905  cdlemefr29clN  40906  cdlemefr32fvaN  40908  cdlemefr32fva1  40909  cdlemg31b0N  41193  cdlemg31b0a  41194  cdlemh  41316  dihmeetlem16N  41821  dihmeetlem18N  41823  dihmeetlem19N  41824  dihmeetlem20N  41825  hoidmvlelem1  47045