Theorem syl311anc 1380

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  syl312anc  1387  syl321anc  1388  syl313anc  1390  syl331anc  1391  pythagtrip  16165  nmolb2d  23321  nmoleub  23334  clwwisshclwwslem  27786  numclwwlk1lem2foa  28127  fprlem1  33132  cvlcvr1  36469  4atlem12b  36741  dalawlem10  37010  dalawlem13  37013  dalawlem15  37015  osumcllem11N  37096  lhp2atne  37164  lhp2at0ne  37166  cdlemd  37337  ltrneq3  37338  cdleme7d  37376  cdlemeg49le  37641  cdleme  37690  cdlemg1a  37700  ltrniotavalbN  37714  cdlemg44  37863  cdlemk19  37999  cdlemk27-3  38037  cdlemk33N  38039  cdlemk34  38040  cdlemk49  38081  cdlemk53a  38085  cdlemk19u  38100  cdlemk56w  38103  dia2dimlem4  38197  dih1dimatlem0  38458  itsclc0yqe  44741  itsclinecirc0  44753  itsclinecirc0b  44754  inlinecirc02plem  44766