Theorem syl311anc 1412

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 1399	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  1419  syl321anc  1420  syl313anc  1422  syl331anc  1423  fprlem1  8356  pythagtrip  17056  nmolb2d  25092  nmoleub  25105  clwwisshclwwslem  30662  numclwwlk1lem2foa  31012  cvlcvr1  40662  4atlem12b  40934  dalawlem10  41203  dalawlem13  41206  dalawlem15  41208  osumcllem11N  41289  lhp2atne  41357  lhp2at0ne  41359  cdlemd  41530  ltrneq3  41531  cdleme7d  41569  cdlemeg49le  41834  cdleme  41883  cdlemg1a  41893  ltrniotavalbN  41907  cdlemg44  42056  cdlemk19  42192  cdlemk27-3  42230  cdlemk33N  42232  cdlemk34  42233  cdlemk49  42274  cdlemk53a  42278  cdlemk19u  42293  cdlemk56w  42296  dia2dimlem4  42390  dih1dimatlem0  42651  itsclc0yqe  50204  itsclinecirc0  50216  itsclinecirc0b  50217  itscnhlinecirc02p  50228  inlinecirc02plem  50229