Theorem syl321anc 1415

Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl321anc.7	⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)

Assertion

Ref	Expression
syl321anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl321anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. . 3 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6	4, 5	jca 520	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl321anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)
9	1, 2, 3, 6, 7, 8	syl311anc 1407	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl322anc  1421  cxple2ad  26848  chordthmlem3  26957  nosupbnd1lem3  27832  nosupbnd1lem4  27833  noinfbnd1lem3  27847  noinfbnd1lem4  27848  4noncolr2  40090  4noncolr1  40091  3atlem5  40123  2lplnj  40256  llnmod2i2  40499  dalawlem11  40517  dalawlem12  40518  cdleme43dN  41128  cdleme4gfv  41143  cdlemeg46nlpq  41153  cdlemg17bq  41309  cdlemg31b0N  41330  cdlemg31b0a  41331  cdlemg31c  41335  cdlemg39  41352  cdlemk47  41585  lincext3  49087