Theorem syl311anc 1411

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 1105

This theorem is referenced by:  syl312anc  1418  syl321anc  1419  syl313anc  1421  syl331anc  1422  fprlem1  8298  pythagtrip  16895  nmolb2d  24856  nmoleub  24869  clwwisshclwwslem  30346  numclwwlk1lem2foa  30686  cvlcvr1  40094  4atlem12b  40366  dalawlem10  40635  dalawlem13  40638  dalawlem15  40640  osumcllem11N  40721  lhp2atne  40789  lhp2at0ne  40791  cdlemd  40962  ltrneq3  40963  cdleme7d  41001  cdlemeg49le  41266  cdleme  41315  cdlemg1a  41325  ltrniotavalbN  41339  cdlemg44  41488  cdlemk19  41624  cdlemk27-3  41662  cdlemk33N  41664  cdlemk34  41665  cdlemk49  41706  cdlemk53a  41710  cdlemk19u  41725  cdlemk56w  41728  dia2dimlem4  41822  dih1dimatlem0  42083  itsclc0yqe  49524  itsclinecirc0  49536  itsclinecirc0b  49537  inlinecirc02plem  49549