Theorem syl331anc 1394

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 1127	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂 ∧ 𝜁))
8		syl133anc.7	. 2 ⊢ (𝜑 → 𝜎)
9		syl331anc.8	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌)
10	1, 2, 3, 7, 8, 9	syl311anc 1383	1 ⊢ (𝜑 → 𝜌)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  syl332anc  1400  syl333anc  1401  qredeu  16692  brbtwn2  28935  3atlem4  39469  3atlem6  39471  llnexchb2  39852  osumcllem9N  39947  cdlemd4  40184  cdleme26fALTN  40345  cdleme26f  40346  cdleme36m  40444  cdlemg17b  40645  cdlemg17h  40651  cdlemk38  40898  cdlemk53b  40939  cdlemkyyN  40945  cdlemk43N  40946