Theorem syl123anc 1389

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  dvfsumlem2  25990  dvfsumlem2OLD  25991  noinfbnd2  27700  atbtwnexOLDN  39471  atbtwnex  39472  osumcllem7N  39986  lhpmcvr5N  40051  cdleme22f2  40371  cdlemefs32sn1aw  40438  cdlemg7aN  40649  cdlemg7N  40650  cdlemg8c  40653  cdlemg8  40655  cdlemg11aq  40662  cdlemg12b  40668  cdlemg12e  40671  cdlemg12g  40673  cdlemg13a  40675  cdlemg15a  40679  cdlemg17e  40689  cdlemg18d  40705  cdlemg19a  40707  cdlemg20  40709  cdlemg22  40711  cdlemg28a  40717  cdlemg29  40729  cdlemg44a  40755  cdlemk34  40934  cdlemn11pre  41234  dihord10  41247  dihord2pre  41249  dihmeetlem17N  41347