Theorem syl311anc 1384

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 1128	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl311anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)
8	4, 5, 6, 7	syl3anc 1371	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 206  df-an 397  df-3an 1089

This theorem is referenced by:  syl312anc  1391  syl321anc  1392  syl313anc  1394  syl331anc  1395  fprlem1  8281  pythagtrip  16763  nmolb2d  24226  nmoleub  24239  clwwisshclwwslem  29256  numclwwlk1lem2foa  29596  cvlcvr1  38197  4atlem12b  38470  dalawlem10  38739  dalawlem13  38742  dalawlem15  38744  osumcllem11N  38825  lhp2atne  38893  lhp2at0ne  38895  cdlemd  39066  ltrneq3  39067  cdleme7d  39105  cdlemeg49le  39370  cdleme  39419  cdlemg1a  39429  ltrniotavalbN  39443  cdlemg44  39592  cdlemk19  39728  cdlemk27-3  39766  cdlemk33N  39768  cdlemk34  39769  cdlemk49  39810  cdlemk53a  39814  cdlemk19u  39829  cdlemk56w  39832  dia2dimlem4  39926  dih1dimatlem0  40187  itsclc0yqe  47400  itsclinecirc0  47412  itsclinecirc0b  47413  inlinecirc02plem  47425