Theorem syl331anc 1418

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl332anc  1424  syl333anc  1425  qredeu  16704  brbtwn2  29160  3atlem4  40117  3atlem6  40119  llnexchb2  40500  osumcllem9N  40595  cdlemd4  40832  cdleme26fALTN  40993  cdleme26f  40994  cdleme36m  41092  cdlemg17b  41293  cdlemg17h  41299  cdlemk38  41546  cdlemk53b  41587  cdlemkyyN  41593  cdlemk43N  41594