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  8239  pythagtrip  16753  nmolb2d  24653  nmoleub  24666  clwwisshclwwslem  30015  numclwwlk1lem2foa  30355  cvlcvr1  39511  4atlem12b  39783  dalawlem10  40052  dalawlem13  40055  dalawlem15  40057  osumcllem11N  40138  lhp2atne  40206  lhp2at0ne  40208  cdlemd  40379  ltrneq3  40380  cdleme7d  40418  cdlemeg49le  40683  cdleme  40732  cdlemg1a  40742  ltrniotavalbN  40756  cdlemg44  40905  cdlemk19  41041  cdlemk27-3  41079  cdlemk33N  41081  cdlemk34  41082  cdlemk49  41123  cdlemk53a  41127  cdlemk19u  41142  cdlemk56w  41145  dia2dimlem4  41239  dih1dimatlem0  41500  itsclc0yqe  48923  itsclinecirc0  48935  itsclinecirc0b  48936  inlinecirc02plem  48948