Theorem syl311anc 1452

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

Syntax hints:   → wi 4   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  syl312anc  1459  syl321anc  1460  syl313anc  1462  syl331anc  1463  pythagtrip  15943  nmolb2d  22930  nmoleub  22943  clwwisshclwwslem  27403  numclwwlk1lem2foa  27783  numclwwlk1lem2foaOLD  27784  cvlcvr1  35487  4atlem12b  35759  dalawlem10  36028  dalawlem13  36031  dalawlem15  36033  osumcllem11N  36114  lhp2atne  36182  lhp2at0ne  36184  cdlemd  36355  ltrneq3  36356  cdleme7d  36394  cdlemeg49le  36659  cdleme  36708  cdlemg1a  36718  ltrniotavalbN  36732  cdlemg44  36881  cdlemk19  37017  cdlemk27-3  37055  cdlemk33N  37057  cdlemk34  37058  cdlemk49  37099  cdlemk53a  37103  cdlemk19u  37118  cdlemk56w  37121  dia2dimlem4  37215  dih1dimatlem0  37476  itsclc0yqe  43489  itsclinecirc0  43501  itsclinecirc0b  43502  inlinecirc02plem  43514