Theorem syl311anc 1381

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 1086

This theorem is referenced by:  syl312anc  1388  syl321anc  1389  syl313anc  1391  syl331anc  1392  fprlem1  8306  pythagtrip  16806  nmolb2d  24679  nmoleub  24692  clwwisshclwwslem  29896  numclwwlk1lem2foa  30236  cvlcvr1  38941  4atlem12b  39214  dalawlem10  39483  dalawlem13  39486  dalawlem15  39488  osumcllem11N  39569  lhp2atne  39637  lhp2at0ne  39639  cdlemd  39810  ltrneq3  39811  cdleme7d  39849  cdlemeg49le  40114  cdleme  40163  cdlemg1a  40173  ltrniotavalbN  40187  cdlemg44  40336  cdlemk19  40472  cdlemk27-3  40510  cdlemk33N  40512  cdlemk34  40513  cdlemk49  40554  cdlemk53a  40558  cdlemk19u  40573  cdlemk56w  40576  dia2dimlem4  40670  dih1dimatlem0  40931  itsclc0yqe  48020  itsclinecirc0  48032  itsclinecirc0b  48033  inlinecirc02plem  48045