Theorem syl311anc 1489

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

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl311anc.6	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)

Assertion

Ref	Expression
syl311anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl311anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1121	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl311anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)
8	4, 5, 6, 7	syl3anc 1475	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1070

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 197  df-an 383  df-3an 1072

This theorem is referenced by:  syl312anc  1496  syl321anc  1497  syl313anc  1499  syl331anc  1500  pythagtrip  15745  nmolb2d  22741  nmoleub  22754  clwwisshclwwslem  27161  numclwlk1lem2foa  27538  cvlcvr1  35141  4atlem12b  35412  dalawlem10  35681  dalawlem13  35684  dalawlem15  35686  osumcllem11N  35767  lhp2atne  35835  lhp2at0ne  35837  cdlemd  36009  ltrneq3  36010  cdleme7d  36048  cdlemeg49le  36313  cdleme  36362  cdlemg1a  36372  ltrniotavalbN  36386  cdlemg44  36535  cdlemk19  36671  cdlemk27-3  36709  cdlemk33N  36711  cdlemk34  36712  cdlemk49  36753  cdlemk53a  36757  cdlemk19u  36772  cdlemk56w  36775  dia2dimlem4  36870  dih1dimatlem0  37131