Theorem syl311anc 1383

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

Hypotheses

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

Assertion

Ref	Expression
syl311anc	⊢ (𝜑 → 𝜁)

Proof of Theorem syl311anc

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 206  df-an 396  df-3an 1088

This theorem is referenced by:  syl312anc  1390  syl321anc  1391  syl313anc  1393  syl331anc  1394  fprlem1  8288  pythagtrip  16772  nmolb2d  24456  nmoleub  24469  clwwisshclwwslem  29531  numclwwlk1lem2foa  29871  cvlcvr1  38513  4atlem12b  38786  dalawlem10  39055  dalawlem13  39058  dalawlem15  39060  osumcllem11N  39141  lhp2atne  39209  lhp2at0ne  39211  cdlemd  39382  ltrneq3  39383  cdleme7d  39421  cdlemeg49le  39686  cdleme  39735  cdlemg1a  39745  ltrniotavalbN  39759  cdlemg44  39908  cdlemk19  40044  cdlemk27-3  40082  cdlemk33N  40084  cdlemk34  40085  cdlemk49  40126  cdlemk53a  40130  cdlemk19u  40145  cdlemk56w  40148  dia2dimlem4  40242  dih1dimatlem0  40503  itsclc0yqe  47536  itsclinecirc0  47548  itsclinecirc0b  47549  inlinecirc02plem  47561