Theorem syl311anc 1490

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 1122	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl311anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)
8	4, 5, 6, 7	syl3anc 1476	1 ⊢ (𝜑 → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1071

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 1073

This theorem is referenced by:  syl312anc  1497  syl321anc  1498  syl313anc  1500  syl331anc  1501  pythagtrip  15746  nmolb2d  22742  nmoleub  22755  clwwisshclwwslem  27164  numclwwlk1lem2foa  27540  cvlcvr1  35148  4atlem12b  35419  dalawlem10  35688  dalawlem13  35691  dalawlem15  35693  osumcllem11N  35774  lhp2atne  35842  lhp2at0ne  35844  cdlemd  36016  ltrneq3  36017  cdleme7d  36055  cdlemeg49le  36320  cdleme  36369  cdlemg1a  36379  ltrniotavalbN  36393  cdlemg44  36542  cdlemk19  36678  cdlemk27-3  36716  cdlemk33N  36718  cdlemk34  36719  cdlemk49  36760  cdlemk53a  36764  cdlemk19u  36779  cdlemk56w  36782  dia2dimlem4  36877  dih1dimatlem0  37138