Theorem syl311anc 1381

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  syl312anc  1388  syl321anc  1389  syl313anc  1391  syl331anc  1392  pythagtrip  16161  nmolb2d  23324  nmoleub  23337  clwwisshclwwslem  27799  numclwwlk1lem2foa  28139  fprlem1  33250  cvlcvr1  36635  4atlem12b  36907  dalawlem10  37176  dalawlem13  37179  dalawlem15  37181  osumcllem11N  37262  lhp2atne  37330  lhp2at0ne  37332  cdlemd  37503  ltrneq3  37504  cdleme7d  37542  cdlemeg49le  37807  cdleme  37856  cdlemg1a  37866  ltrniotavalbN  37880  cdlemg44  38029  cdlemk19  38165  cdlemk27-3  38203  cdlemk33N  38205  cdlemk34  38206  cdlemk49  38247  cdlemk53a  38251  cdlemk19u  38266  cdlemk56w  38269  dia2dimlem4  38363  dih1dimatlem0  38624  itsclc0yqe  45175  itsclinecirc0  45187  itsclinecirc0b  45188  inlinecirc02plem  45200