Theorem syl311anc 1340

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

Syntax hints:   → wi 4   ∧ w3a 1037

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 386  df-3an 1039

This theorem is referenced by:  syl312anc  1347  syl321anc  1348  syl313anc  1350  syl331anc  1351  pythagtrip  15539  nmolb2d  22522  nmoleub  22535  clwwisshclwwslem  26927  cvlcvr1  34626  4atlem12b  34897  dalawlem10  35166  dalawlem13  35169  dalawlem15  35171  osumcllem11N  35252  lhp2atne  35320  lhp2at0ne  35322  cdlemd  35494  ltrneq3  35495  cdleme7d  35533  cdlemeg49le  35799  cdleme  35848  cdlemg1a  35858  ltrniotavalbN  35872  cdlemg44  36021  cdlemk19  36157  cdlemk27-3  36195  cdlemk33N  36197  cdlemk34  36198  cdlemk49  36239  cdlemk53a  36243  cdlemk19u  36258  cdlemk56w  36261  dia2dimlem4  36356  dih1dimatlem0  36617