Theorem syl311anc 1332

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl312anc  1339  syl321anc  1340  syl313anc  1342  syl331anc  1343  pythagtrip  15377  nmolb2d  22332  nmoleub  22345  clwwisshclwwlem  26334  cvlcvr1  33644  4atlem12b  33915  dalawlem10  34184  dalawlem13  34187  dalawlem15  34189  osumcllem11N  34270  lhp2atne  34338  lhp2at0ne  34340  cdlemd  34512  ltrneq3  34513  cdleme7d  34551  cdlemeg49le  34817  cdleme  34866  cdlemg1a  34876  ltrniotavalbN  34890  cdlemg44  35039  cdlemk19  35175  cdlemk27-3  35213  cdlemk33N  35215  cdlemk34  35216  cdlemk49  35257  cdlemk53a  35261  cdlemk19u  35276  cdlemk56w  35279  dia2dimlem4  35374  dih1dimatlem0  35635  clwwisshclwwslem  41234