Theorem syl123anc 1335

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

Hypotheses

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

Assertion

Ref	Expression
syl123anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl123anc

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  dvfsumlem2  23594  atbtwnexOLDN  33751  atbtwnex  33752  osumcllem7N  34266  lhpmcvr5N  34331  cdleme22f2  34653  cdlemefs32sn1aw  34720  cdlemg7aN  34931  cdlemg7N  34932  cdlemg8c  34935  cdlemg8  34937  cdlemg11aq  34944  cdlemg12b  34950  cdlemg12e  34953  cdlemg12g  34955  cdlemg13a  34957  cdlemg15a  34961  cdlemg17e  34971  cdlemg18d  34987  cdlemg19a  34989  cdlemg20  34991  cdlemg22  34993  cdlemg28a  34999  cdlemg29  35011  cdlemg44a  35037  cdlemk34  35216  cdlemn11pre  35517  dihord10  35530  dihord2pre  35532  dihmeetlem17N  35630