Theorem syl123anc 1343

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

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.4	|- ( ph -> ta )
syl23anc.5	|- ( ph -> et )
syl33anc.6	|- ( ph -> ze )
syl123anc.7	|- ( ( ps /\ ( ch /\ th ) /\ ( ta /\ et /\ ze ) ) -> si )

Assertion

Ref	Expression
syl123anc	|- ( ph -> si )

Proof of Theorem syl123anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 |- ( ph -> ps )
2		syl12anc.2	. . 3 |- ( ph -> ch )
3		syl12anc.3	. . 3 |- ( ph -> th )
4	2, 3	jca 554	. 2 |- ( ph -> ( ch /\ th ) )
5		syl22anc.4	. 2 |- ( ph -> ta )
6		syl23anc.5	. 2 |- ( ph -> et )
7		syl33anc.6	. 2 |- ( ph -> ze )
8		syl123anc.7	. 2 |- ( ( ps /\ ( ch /\ th ) /\ ( ta /\ et /\ ze ) ) -> si )
9	1, 4, 5, 6, 7, 8	syl113anc 1338	1 |- ( ph -> si )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  dvfsumlem2  23790  atbtwnexOLDN  34733  atbtwnex  34734  osumcllem7N  35248  lhpmcvr5N  35313  cdleme22f2  35635  cdlemefs32sn1aw  35702  cdlemg7aN  35913  cdlemg7N  35914  cdlemg8c  35917  cdlemg8  35919  cdlemg11aq  35926  cdlemg12b  35932  cdlemg12e  35935  cdlemg12g  35937  cdlemg13a  35939  cdlemg15a  35943  cdlemg17e  35953  cdlemg18d  35969  cdlemg19a  35971  cdlemg20  35973  cdlemg22  35975  cdlemg28a  35981  cdlemg29  35993  cdlemg44a  36019  cdlemk34  36198  cdlemn11pre  36499  dihord10  36512  dihord2pre  36514  dihmeetlem17N  36612