Theorem syl311anc 1386

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 1373	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  1393  syl321anc  1394  syl313anc  1396  syl331anc  1397  fprlem1  8325  pythagtrip  16872  nmolb2d  24739  nmoleub  24752  clwwisshclwwslem  30033  numclwwlk1lem2foa  30373  cvlcvr1  39340  4atlem12b  39613  dalawlem10  39882  dalawlem13  39885  dalawlem15  39887  osumcllem11N  39968  lhp2atne  40036  lhp2at0ne  40038  cdlemd  40209  ltrneq3  40210  cdleme7d  40248  cdlemeg49le  40513  cdleme  40562  cdlemg1a  40572  ltrniotavalbN  40586  cdlemg44  40735  cdlemk19  40871  cdlemk27-3  40909  cdlemk33N  40911  cdlemk34  40912  cdlemk49  40953  cdlemk53a  40957  cdlemk19u  40972  cdlemk56w  40975  dia2dimlem4  41069  dih1dimatlem0  41330  itsclc0yqe  48682  itsclinecirc0  48694  itsclinecirc0b  48695  inlinecirc02plem  48707