Theorem syl311anc 1409

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl312anc  1416  syl321anc  1417  syl313anc  1419  syl331anc  1420  fprlem1  8293  pythagtrip  16890  nmolb2d  24840  nmoleub  24853  clwwisshclwwslem  30302  numclwwlk1lem2foa  30642  cvlcvr1  39998  4atlem12b  40270  dalawlem10  40539  dalawlem13  40542  dalawlem15  40544  osumcllem11N  40625  lhp2atne  40693  lhp2at0ne  40695  cdlemd  40866  ltrneq3  40867  cdleme7d  40905  cdlemeg49le  41170  cdleme  41219  cdlemg1a  41229  ltrniotavalbN  41243  cdlemg44  41392  cdlemk19  41528  cdlemk27-3  41566  cdlemk33N  41568  cdlemk34  41569  cdlemk49  41610  cdlemk53a  41614  cdlemk19u  41629  cdlemk56w  41632  dia2dimlem4  41726  dih1dimatlem0  41987  itsclc0yqe  49419  itsclinecirc0  49431  itsclinecirc0b  49432  inlinecirc02plem  49444