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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl312anc  1391  syl321anc  1392  syl313anc  1394  syl331anc  1395  fprlem1  8341  pythagtrip  16881  nmolb2d  24760  nmoleub  24773  clwwisshclwwslem  30046  numclwwlk1lem2foa  30386  cvlcvr1  39295  4atlem12b  39568  dalawlem10  39837  dalawlem13  39840  dalawlem15  39842  osumcllem11N  39923  lhp2atne  39991  lhp2at0ne  39993  cdlemd  40164  ltrneq3  40165  cdleme7d  40203  cdlemeg49le  40468  cdleme  40517  cdlemg1a  40527  ltrniotavalbN  40541  cdlemg44  40690  cdlemk19  40826  cdlemk27-3  40864  cdlemk33N  40866  cdlemk34  40867  cdlemk49  40908  cdlemk53a  40912  cdlemk19u  40927  cdlemk56w  40930  dia2dimlem4  41024  dih1dimatlem0  41285  itsclc0yqe  48495  itsclinecirc0  48507  itsclinecirc0b  48508  inlinecirc02plem  48520