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  8299  pythagtrip  16911  nmolb2d  24904  nmoleub  24917  clwwisshclwwslem  30394  numclwwlk1lem2foa  30734  cvlcvr1  40146  4atlem12b  40418  dalawlem10  40687  dalawlem13  40690  dalawlem15  40692  osumcllem11N  40773  lhp2atne  40841  lhp2at0ne  40843  cdlemd  41014  ltrneq3  41015  cdleme7d  41053  cdlemeg49le  41318  cdleme  41367  cdlemg1a  41377  ltrniotavalbN  41391  cdlemg44  41540  cdlemk19  41676  cdlemk27-3  41714  cdlemk33N  41716  cdlemk34  41717  cdlemk49  41758  cdlemk53a  41762  cdlemk19u  41777  cdlemk56w  41780  dia2dimlem4  41874  dih1dimatlem0  42135  itsclc0yqe  49574  itsclinecirc0  49586  itsclinecirc0b  49587  inlinecirc02plem  49599