Theorem syl311anc 1402

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

Syntax hints:   → wi 4   ∧ w3a 1097

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

This theorem is referenced by:  syl312anc  1409  syl321anc  1410  syl313anc  1412  syl331anc  1413  fprlem1  8275  pythagtrip  16861  nmolb2d  24766  nmoleub  24779  clwwisshclwwslem  30173  numclwwlk1lem2foa  30513  cvlcvr1  39924  4atlem12b  40196  dalawlem10  40465  dalawlem13  40468  dalawlem15  40470  osumcllem11N  40551  lhp2atne  40619  lhp2at0ne  40621  cdlemd  40792  ltrneq3  40793  cdleme7d  40831  cdlemeg49le  41096  cdleme  41145  cdlemg1a  41155  ltrniotavalbN  41169  cdlemg44  41318  cdlemk19  41454  cdlemk27-3  41492  cdlemk33N  41494  cdlemk34  41495  cdlemk49  41536  cdlemk53a  41540  cdlemk19u  41555  cdlemk56w  41558  dia2dimlem4  41652  dih1dimatlem0  41913  itsclc0yqe  49344  itsclinecirc0  49356  itsclinecirc0b  49357  inlinecirc02plem  49369