Theorem syl331anc 1391

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  syl332anc  1397  syl333anc  1398  qredeu  16004  brbtwn2  26693  3atlem4  36624  3atlem6  36626  llnexchb2  37007  osumcllem9N  37102  cdlemd4  37339  cdleme26fALTN  37500  cdleme26f  37501  cdleme36m  37599  cdlemg17b  37800  cdlemg17h  37806  cdlemk38  38053  cdlemk53b  38094  cdlemkyyN  38100  cdlemk43N  38101