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 206  df-an 397  df-3an 1088

This theorem is referenced by:  syl312anc  1390  syl321anc  1391  syl313anc  1393  syl331anc  1394  fprlem1  8107  pythagtrip  16533  nmolb2d  23880  nmoleub  23893  clwwisshclwwslem  28374  numclwwlk1lem2foa  28714  cvlcvr1  37349  4atlem12b  37621  dalawlem10  37890  dalawlem13  37893  dalawlem15  37895  osumcllem11N  37976  lhp2atne  38044  lhp2at0ne  38046  cdlemd  38217  ltrneq3  38218  cdleme7d  38256  cdlemeg49le  38521  cdleme  38570  cdlemg1a  38580  ltrniotavalbN  38594  cdlemg44  38743  cdlemk19  38879  cdlemk27-3  38917  cdlemk33N  38919  cdlemk34  38920  cdlemk49  38961  cdlemk53a  38965  cdlemk19u  38980  cdlemk56w  38983  dia2dimlem4  39077  dih1dimatlem0  39338  itsclc0yqe  46076  itsclinecirc0  46088  itsclinecirc0b  46089  inlinecirc02plem  46101