Theorem syl321anc 1390

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 511	. 2 ⊢ (𝜑 → (𝜏 ∧ 𝜂))
7		syl33anc.6	. 2 ⊢ (𝜑 → 𝜁)
8		syl321anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎)
9	1, 2, 3, 6, 7, 8	syl311anc 1382	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 396  df-3an 1087

This theorem is referenced by:  syl322anc  1396  cxple2ad  25785  chordthmlem3  25889  nosupbnd1lem3  33840  nosupbnd1lem4  33841  noinfbnd1lem3  33855  noinfbnd1lem4  33856  4noncolr2  37395  4noncolr1  37396  3atlem5  37428  2lplnj  37561  llnmod2i2  37804  dalawlem11  37822  dalawlem12  37823  cdleme43dN  38433  cdleme4gfv  38448  cdlemeg46nlpq  38458  cdlemg17bq  38614  cdlemg31b0N  38635  cdlemg31b0a  38636  cdlemg31c  38640  cdlemg39  38657  cdlemk47  38890  lincext3  45685