Theorem syl311anc 1386

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

This theorem is referenced by:  syl312anc  1393  syl321anc  1394  syl313anc  1396  syl331anc  1397  fprlem1  8240  pythagtrip  16764  nmolb2d  24622  nmoleub  24635  clwwisshclwwslem  29976  numclwwlk1lem2foa  30316  cvlcvr1  39320  4atlem12b  39593  dalawlem10  39862  dalawlem13  39865  dalawlem15  39867  osumcllem11N  39948  lhp2atne  40016  lhp2at0ne  40018  cdlemd  40189  ltrneq3  40190  cdleme7d  40228  cdlemeg49le  40493  cdleme  40542  cdlemg1a  40552  ltrniotavalbN  40566  cdlemg44  40715  cdlemk19  40851  cdlemk27-3  40889  cdlemk33N  40891  cdlemk34  40892  cdlemk49  40933  cdlemk53a  40937  cdlemk19u  40952  cdlemk56w  40955  dia2dimlem4  41049  dih1dimatlem0  41310  itsclc0yqe  48750  itsclinecirc0  48762  itsclinecirc0b  48763  inlinecirc02plem  48775