Theorem syl331anc 1515

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	⊢ (𝜑 → 𝜁)
syl133anc.7	⊢ (𝜑 → 𝜎)
syl331anc.8	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌)

Assertion

Ref	Expression
syl331anc	⊢ (𝜑 → 𝜌)

Proof of Theorem syl331anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. . 3 ⊢ (𝜑 → 𝜁)
7	4, 5, 6	3jca 1159	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂 ∧ 𝜁))
8		syl133anc.7	. 2 ⊢ (𝜑 → 𝜎)
9		syl331anc.8	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌)
10	1, 2, 3, 7, 8, 9	syl311anc 1504	1 ⊢ (𝜑 → 𝜌)

Syntax hints:   → wi 4   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  syl332anc  1521  syl333anc  1522  qredeu  15703  brbtwn2  26134  3atlem4  35499  3atlem6  35501  llnexchb2  35882  osumcllem9N  35977  cdlemd4  36214  cdleme26fALTN  36375  cdleme26f  36376  cdleme36m  36474  cdlemg17b  36675  cdlemg17h  36681  cdlemk38  36928  cdlemk53b  36969  cdlemkyyN  36975  cdlemk43N  36976