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 ⊢ (𝜑 → 𝜁)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl312anc  1418  syl321anc  1419  syl313anc  1421  syl331anc  1422  fprlem1  8299  pythagtrip  16926  nmolb2d  24944  nmoleub  24957  clwwisshclwwslem  30484  numclwwlk1lem2foa  30834  cvlcvr1  40212  4atlem12b  40484  dalawlem10  40753  dalawlem13  40756  dalawlem15  40758  osumcllem11N  40839  lhp2atne  40907  lhp2at0ne  40909  cdlemd  41080  ltrneq3  41081  cdleme7d  41119  cdlemeg49le  41384  cdleme  41433  cdlemg1a  41443  ltrniotavalbN  41457  cdlemg44  41606  cdlemk19  41742  cdlemk27-3  41780  cdlemk33N  41782  cdlemk34  41783  cdlemk49  41824  cdlemk53a  41828  cdlemk19u  41843  cdlemk56w  41846  dia2dimlem4  41940  dih1dimatlem0  42201  itsclc0yqe  49691  itsclinecirc0  49703  itsclinecirc0b  49704  inlinecirc02plem  49716