Theorem syl311anc 1387

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl312anc  1394  syl321anc  1395  syl313anc  1397  syl331anc  1398  fprlem1  8252  pythagtrip  16774  nmolb2d  24674  nmoleub  24687  clwwisshclwwslem  30101  numclwwlk1lem2foa  30441  cvlcvr1  39712  4atlem12b  39984  dalawlem10  40253  dalawlem13  40256  dalawlem15  40258  osumcllem11N  40339  lhp2atne  40407  lhp2at0ne  40409  cdlemd  40580  ltrneq3  40581  cdleme7d  40619  cdlemeg49le  40884  cdleme  40933  cdlemg1a  40943  ltrniotavalbN  40957  cdlemg44  41106  cdlemk19  41242  cdlemk27-3  41280  cdlemk33N  41282  cdlemk34  41283  cdlemk49  41324  cdlemk53a  41328  cdlemk19u  41343  cdlemk56w  41346  dia2dimlem4  41440  dih1dimatlem0  41701  itsclc0yqe  49118  itsclinecirc0  49130  itsclinecirc0b  49131  inlinecirc02plem  49143