Theorem syl123anc 1395

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

Hypotheses

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

Assertion

Ref	Expression
syl123anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl123anc

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  dvfsumlem2  26019  noinfbnd2  27720  atbtwnexOLDN  39946  atbtwnex  39947  osumcllem7N  40461  lhpmcvr5N  40526  cdleme22f2  40846  cdlemefs32sn1aw  40913  cdlemg7aN  41124  cdlemg7N  41125  cdlemg8c  41128  cdlemg8  41130  cdlemg11aq  41137  cdlemg12b  41143  cdlemg12e  41146  cdlemg12g  41148  cdlemg13a  41150  cdlemg15a  41154  cdlemg17e  41164  cdlemg18d  41180  cdlemg19a  41182  cdlemg20  41184  cdlemg22  41186  cdlemg28a  41192  cdlemg29  41204  cdlemg44a  41230  cdlemk34  41409  cdlemn11pre  41709  dihord10  41722  dihord2pre  41724  dihmeetlem17N  41822