Theorem syl311anc 1411

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 1146	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl311anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)
8	4, 5, 6, 7	syl3anc 1398	1 ⊢ (𝜑 → 𝜁)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl312anc  1418  syl321anc  1419  syl313anc  1421  syl331anc  1422  fprlem1  8311  pythagtrip  17005  nmolb2d  25030  nmoleub  25043  clwwisshclwwslem  30598  numclwwlk1lem2foa  30948  cvlcvr1  40376  4atlem12b  40648  dalawlem10  40917  dalawlem13  40920  dalawlem15  40922  osumcllem11N  41003  lhp2atne  41071  lhp2at0ne  41073  cdlemd  41244  ltrneq3  41245  cdleme7d  41283  cdlemeg49le  41548  cdleme  41597  cdlemg1a  41607  ltrniotavalbN  41621  cdlemg44  41770  cdlemk19  41906  cdlemk27-3  41944  cdlemk33N  41946  cdlemk34  41947  cdlemk49  41988  cdlemk53a  41992  cdlemk19u  42007  cdlemk56w  42010  dia2dimlem4  42104  dih1dimatlem0  42365  itsclc0yqe  49842  itsclinecirc0  49854  itsclinecirc0b  49855  inlinecirc02plem  49867