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 1128	. 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 1086

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 1088

This theorem is referenced by:  syl312anc  1393  syl321anc  1394  syl313anc  1396  syl331anc  1397  fprlem1  8299  pythagtrip  16854  nmolb2d  24657  nmoleub  24670  clwwisshclwwslem  29995  numclwwlk1lem2foa  30335  cvlcvr1  39357  4atlem12b  39630  dalawlem10  39899  dalawlem13  39902  dalawlem15  39904  osumcllem11N  39985  lhp2atne  40053  lhp2at0ne  40055  cdlemd  40226  ltrneq3  40227  cdleme7d  40265  cdlemeg49le  40530  cdleme  40579  cdlemg1a  40589  ltrniotavalbN  40603  cdlemg44  40752  cdlemk19  40888  cdlemk27-3  40926  cdlemk33N  40928  cdlemk34  40929  cdlemk49  40970  cdlemk53a  40974  cdlemk19u  40989  cdlemk56w  40992  dia2dimlem4  41086  dih1dimatlem0  41347  itsclc0yqe  48741  itsclinecirc0  48753  itsclinecirc0b  48754  inlinecirc02plem  48766