Theorem syl311anc 1382

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  syl312anc  1389  syl321anc  1390  syl313anc  1392  syl331anc  1393  fprlem1  8287  pythagtrip  16771  nmolb2d  24455  nmoleub  24468  clwwisshclwwslem  29534  numclwwlk1lem2foa  29874  cvlcvr1  38512  4atlem12b  38785  dalawlem10  39054  dalawlem13  39057  dalawlem15  39059  osumcllem11N  39140  lhp2atne  39208  lhp2at0ne  39210  cdlemd  39381  ltrneq3  39382  cdleme7d  39420  cdlemeg49le  39685  cdleme  39734  cdlemg1a  39744  ltrniotavalbN  39758  cdlemg44  39907  cdlemk19  40043  cdlemk27-3  40081  cdlemk33N  40083  cdlemk34  40084  cdlemk49  40125  cdlemk53a  40129  cdlemk19u  40144  cdlemk56w  40147  dia2dimlem4  40241  dih1dimatlem0  40502  itsclc0yqe  47534  itsclinecirc0  47546  itsclinecirc0b  47547  inlinecirc02plem  47559