Theorem syl33anc 1403

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  xpord3inddlem  8129  initoeu2lem2  18031  mdetunilem9  22660  mdetuni0  22661  xmetrtri  24395  bl2in  24440  blhalf  24445  blssps  24464  blss  24465  blcld  24545  methaus  24560  metdstri  24892  metdscnlem  24896  metnrmlem3  24902  xlebnum  25007  pmltpclem1  25490  bdayfinbndlem1  28537  colinearalglem2  29054  axlowdim  29108  ssbnd  38251  totbndbnd  38252  heiborlem6  38279  2atm  40115  lplncvrlvol2  40203  dalem19  40270  paddasslem9  40416  pclclN  40479  pclfinN  40488  pclfinclN  40538  pexmidlem8N  40565  trlval3  40775  cdleme22b  40929  cdlemefr29bpre0N  40994  cdlemefr29clN  40995  cdlemefr32fvaN  40997  cdlemefr32fva1  40998  cdlemg31b0N  41282  cdlemg31b0a  41283  cdlemh  41405  dihmeetlem16N  41910  dihmeetlem18N  41912  dihmeetlem19N  41913  dihmeetlem20N  41914  hoidmvlelem1  47133