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  8279  pythagtrip  16805  nmolb2d  24606  nmoleub  24619  clwwisshclwwslem  29943  numclwwlk1lem2foa  30283  cvlcvr1  39332  4atlem12b  39605  dalawlem10  39874  dalawlem13  39877  dalawlem15  39879  osumcllem11N  39960  lhp2atne  40028  lhp2at0ne  40030  cdlemd  40201  ltrneq3  40202  cdleme7d  40240  cdlemeg49le  40505  cdleme  40554  cdlemg1a  40564  ltrniotavalbN  40578  cdlemg44  40727  cdlemk19  40863  cdlemk27-3  40901  cdlemk33N  40903  cdlemk34  40904  cdlemk49  40945  cdlemk53a  40949  cdlemk19u  40964  cdlemk56w  40967  dia2dimlem4  41061  dih1dimatlem0  41322  itsclc0yqe  48750  itsclinecirc0  48762  itsclinecirc0b  48763  inlinecirc02plem  48775