Theorem syl231anc 1383

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

Assertion

Ref	Expression
syl231anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl231anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 512	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl231anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)
9	3, 4, 5, 6, 7, 8	syl131anc 1376	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 1082

This theorem is referenced by:  syl232anc  1390  isosctr  25080  axeuclid  26432  dalawlem3  36540  dalawlem6  36543  cdlemd7  36871  cdleme18c  36960  cdlemi  37487  cdlemk7  37515  cdlemk11  37516  cdlemk7u  37537  cdlemk11u  37538  cdlemk19xlem  37609  cdlemk55u1  37632  cdlemk56  37638