Theorem syl311anc 1382

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 1087

This theorem is referenced by:  syl312anc  1389  syl321anc  1390  syl313anc  1392  syl331anc  1393  fprlem1  8100  pythagtrip  16516  nmolb2d  23863  nmoleub  23876  clwwisshclwwslem  28357  numclwwlk1lem2foa  28697  cvlcvr1  37332  4atlem12b  37604  dalawlem10  37873  dalawlem13  37876  dalawlem15  37878  osumcllem11N  37959  lhp2atne  38027  lhp2at0ne  38029  cdlemd  38200  ltrneq3  38201  cdleme7d  38239  cdlemeg49le  38504  cdleme  38553  cdlemg1a  38563  ltrniotavalbN  38577  cdlemg44  38726  cdlemk19  38862  cdlemk27-3  38900  cdlemk33N  38902  cdlemk34  38903  cdlemk49  38944  cdlemk53a  38948  cdlemk19u  38963  cdlemk56w  38966  dia2dimlem4  39060  dih1dimatlem0  39321  itsclc0yqe  46059  itsclinecirc0  46071  itsclinecirc0b  46072  inlinecirc02plem  46084