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  8243  pythagtrip  16796  nmolb2d  24693  nmoleub  24706  clwwisshclwwslem  30099  numclwwlk1lem2foa  30439  cvlcvr1  39799  4atlem12b  40071  dalawlem10  40340  dalawlem13  40343  dalawlem15  40345  osumcllem11N  40426  lhp2atne  40494  lhp2at0ne  40496  cdlemd  40667  ltrneq3  40668  cdleme7d  40706  cdlemeg49le  40971  cdleme  41020  cdlemg1a  41030  ltrniotavalbN  41044  cdlemg44  41193  cdlemk19  41329  cdlemk27-3  41367  cdlemk33N  41369  cdlemk34  41370  cdlemk49  41411  cdlemk53a  41415  cdlemk19u  41430  cdlemk56w  41433  dia2dimlem4  41527  dih1dimatlem0  41788  itsclc0yqe  49249  itsclinecirc0  49261  itsclinecirc0b  49262  inlinecirc02plem  49274