Theorem syl311anc 1392

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl312anc  1399  syl321anc  1400  syl313anc  1402  syl331anc  1403  fprlem1  8240  pythagtrip  16796  nmolb2d  24701  nmoleub  24714  clwwisshclwwslem  30102  numclwwlk1lem2foa  30442  cvlcvr1  39831  4atlem12b  40103  dalawlem10  40372  dalawlem13  40375  dalawlem15  40377  osumcllem11N  40458  lhp2atne  40526  lhp2at0ne  40528  cdlemd  40699  ltrneq3  40700  cdleme7d  40738  cdlemeg49le  41003  cdleme  41052  cdlemg1a  41062  ltrniotavalbN  41076  cdlemg44  41225  cdlemk19  41361  cdlemk27-3  41399  cdlemk33N  41401  cdlemk34  41402  cdlemk49  41443  cdlemk53a  41447  cdlemk19u  41462  cdlemk56w  41465  dia2dimlem4  41559  dih1dimatlem0  41820  itsclc0yqe  49252  itsclinecirc0  49264  itsclinecirc0b  49265  inlinecirc02plem  49277