Theorem syl311anc 1383

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 1127	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl23anc.5	. 2 ⊢ (𝜑 → 𝜂)
7		syl311anc.6	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁)
8	4, 5, 6, 7	syl3anc 1370	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  1390  syl321anc  1391  syl313anc  1393  syl331anc  1394  fprlem1  8324  pythagtrip  16868  nmolb2d  24755  nmoleub  24768  clwwisshclwwslem  30043  numclwwlk1lem2foa  30383  cvlcvr1  39321  4atlem12b  39594  dalawlem10  39863  dalawlem13  39866  dalawlem15  39868  osumcllem11N  39949  lhp2atne  40017  lhp2at0ne  40019  cdlemd  40190  ltrneq3  40191  cdleme7d  40229  cdlemeg49le  40494  cdleme  40543  cdlemg1a  40553  ltrniotavalbN  40567  cdlemg44  40716  cdlemk19  40852  cdlemk27-3  40890  cdlemk33N  40892  cdlemk34  40893  cdlemk49  40934  cdlemk53a  40938  cdlemk19u  40953  cdlemk56w  40956  dia2dimlem4  41050  dih1dimatlem0  41311  itsclc0yqe  48611  itsclinecirc0  48623  itsclinecirc0b  48624  inlinecirc02plem  48636