Theorem syl123anc 1386

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

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

This theorem is referenced by:  dvfsumlem2  25200  noinfbnd2  33943  atbtwnexOLDN  37468  atbtwnex  37469  osumcllem7N  37983  lhpmcvr5N  38048  cdleme22f2  38368  cdlemefs32sn1aw  38435  cdlemg7aN  38646  cdlemg7N  38647  cdlemg8c  38650  cdlemg8  38652  cdlemg11aq  38659  cdlemg12b  38665  cdlemg12e  38668  cdlemg12g  38670  cdlemg13a  38672  cdlemg15a  38676  cdlemg17e  38686  cdlemg18d  38702  cdlemg19a  38704  cdlemg20  38706  cdlemg22  38708  cdlemg28a  38714  cdlemg29  38726  cdlemg44a  38752  cdlemk34  38931  cdlemn11pre  39231  dihord10  39244  dihord2pre  39246  dihmeetlem17N  39344