Theorem syl311anc 1399

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

Syntax hints:   → wi 4   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  syl312anc  1406  syl321anc  1407  syl313anc  1409  syl331anc  1410  fprlem1  8269  pythagtrip  16846  nmolb2d  24751  nmoleub  24764  clwwisshclwwslem  30155  numclwwlk1lem2foa  30495  cvlcvr1  39911  4atlem12b  40183  dalawlem10  40452  dalawlem13  40455  dalawlem15  40457  osumcllem11N  40538  lhp2atne  40606  lhp2at0ne  40608  cdlemd  40779  ltrneq3  40780  cdleme7d  40818  cdlemeg49le  41083  cdleme  41132  cdlemg1a  41142  ltrniotavalbN  41156  cdlemg44  41305  cdlemk19  41441  cdlemk27-3  41479  cdlemk33N  41481  cdlemk34  41482  cdlemk49  41523  cdlemk53a  41527  cdlemk19u  41542  cdlemk56w  41545  dia2dimlem4  41639  dih1dimatlem0  41900  itsclc0yqe  49331  itsclinecirc0  49343  itsclinecirc0b  49344  inlinecirc02plem  49356