Theorem syl311anc 1387

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl312anc  1394  syl321anc  1395  syl313anc  1397  syl331anc  1398  fprlem1  8250  pythagtrip  16805  nmolb2d  24683  nmoleub  24696  clwwisshclwwslem  30084  numclwwlk1lem2foa  30424  cvlcvr1  39785  4atlem12b  40057  dalawlem10  40326  dalawlem13  40329  dalawlem15  40331  osumcllem11N  40412  lhp2atne  40480  lhp2at0ne  40482  cdlemd  40653  ltrneq3  40654  cdleme7d  40692  cdlemeg49le  40957  cdleme  41006  cdlemg1a  41016  ltrniotavalbN  41030  cdlemg44  41179  cdlemk19  41315  cdlemk27-3  41353  cdlemk33N  41355  cdlemk34  41356  cdlemk49  41397  cdlemk53a  41401  cdlemk19u  41416  cdlemk56w  41419  dia2dimlem4  41513  dih1dimatlem0  41774  itsclc0yqe  49237  itsclinecirc0  49249  itsclinecirc0b  49250  inlinecirc02plem  49262