Theorem syl123anc 1383

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 514	. 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 1378	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 1085

This theorem is referenced by:  dvfsumlem2  24627  atbtwnexOLDN  36587  atbtwnex  36588  osumcllem7N  37102  lhpmcvr5N  37167  cdleme22f2  37487  cdlemefs32sn1aw  37554  cdlemg7aN  37765  cdlemg7N  37766  cdlemg8c  37769  cdlemg8  37771  cdlemg11aq  37778  cdlemg12b  37784  cdlemg12e  37787  cdlemg12g  37789  cdlemg13a  37791  cdlemg15a  37795  cdlemg17e  37805  cdlemg18d  37821  cdlemg19a  37823  cdlemg20  37825  cdlemg22  37827  cdlemg28a  37833  cdlemg29  37845  cdlemg44a  37871  cdlemk34  38050  cdlemn11pre  38350  dihord10  38363  dihord2pre  38365  dihmeetlem17N  38463