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  16173  nmolb2d  23329  nmoleub  23342  clwwisshclwwslem  27794  numclwwlk1lem2foa  28135  fprlem1  33139  cvlcvr1  36477  4atlem12b  36749  dalawlem10  37018  dalawlem13  37021  dalawlem15  37023  osumcllem11N  37104  lhp2atne  37172  lhp2at0ne  37174  cdlemd  37345  ltrneq3  37346  cdleme7d  37384  cdlemeg49le  37649  cdleme  37698  cdlemg1a  37708  ltrniotavalbN  37722  cdlemg44  37871  cdlemk19  38007  cdlemk27-3  38045  cdlemk33N  38047  cdlemk34  38048  cdlemk49  38089  cdlemk53a  38093  cdlemk19u  38108  cdlemk56w  38111  dia2dimlem4  38205  dih1dimatlem0  38466  itsclc0yqe  44755  itsclinecirc0  44767  itsclinecirc0b  44768  inlinecirc02plem  44780