Theorem syl312anc 1418

Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl312anc.7	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎)

Assertion

Ref	Expression
syl312anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl312anc

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pythagtriplem19  17011  flt4lem5c  27984  flt4lem5d  27985  flt4lem5e  27986  cdleme27cl  41424  cdlemefs27cl  41471  cdleme32fvcl  41498  cdlemg16ALTN  41716  cdlemg27a  41750  cdlemg31c  41757  cdlemg39  41774  cdlemk11ta  41987  cdlemk19ylem  41988  cdlemk11tc  42003  cdlemk45  42005  dihmeetlem12N  42376  dihjatc  42475