Theorem syl311anc 1384

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 1128	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl311anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)
8	4, 5, 6, 7	syl3anc 1371	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 206  df-an 398  df-3an 1089

This theorem is referenced by:  syl312anc  1391  syl321anc  1392  syl313anc  1394  syl331anc  1395  fprlem1  8147  pythagtrip  16580  nmolb2d  23927  nmoleub  23940  clwwisshclwwslem  28423  numclwwlk1lem2foa  28763  cvlcvr1  37395  4atlem12b  37667  dalawlem10  37936  dalawlem13  37939  dalawlem15  37941  osumcllem11N  38022  lhp2atne  38090  lhp2at0ne  38092  cdlemd  38263  ltrneq3  38264  cdleme7d  38302  cdlemeg49le  38567  cdleme  38616  cdlemg1a  38626  ltrniotavalbN  38640  cdlemg44  38789  cdlemk19  38925  cdlemk27-3  38963  cdlemk33N  38965  cdlemk34  38966  cdlemk49  39007  cdlemk53a  39011  cdlemk19u  39026  cdlemk56w  39029  dia2dimlem4  39123  dih1dimatlem0  39384  itsclc0yqe  46165  itsclinecirc0  46177  itsclinecirc0b  46178  inlinecirc02plem  46190