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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl332anc  1409  syl333anc  1410  qredeu  16625  brbtwn2  28999  3atlem4  39985  3atlem6  39987  llnexchb2  40368  osumcllem9N  40463  cdlemd4  40700  cdleme26fALTN  40861  cdleme26f  40862  cdleme36m  40960  cdlemg17b  41161  cdlemg17h  41167  cdlemk38  41414  cdlemk53b  41455  cdlemkyyN  41461  cdlemk43N  41462