Theorem syl311anc 1199

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

Hypotheses

Ref	Expression
sylXanc.1	|- ( ph -> ps )
sylXanc.2	|- ( ph -> ch )
sylXanc.3	|- ( ph -> th )
sylXanc.4	|- ( ph -> ta )
sylXanc.5	|- ( ph -> et )
syl311anc.6	|- ( ( ( ps /\ ch /\ th ) /\ ta /\ et ) -> ze )

Assertion

Ref	Expression
syl311anc	|- ( ph -> ze )

Proof of Theorem syl311anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 |- ( ph -> ps )
2		sylXanc.2	. . 3 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4	1, 2, 3	3jca 1135	. 2 |- ( ph -> ( ps /\ ch /\ th ) )
5		sylXanc.4	. 2 |- ( ph -> ta )
6		sylXanc.5	. 2 |- ( ph -> et )
7		syl311anc.6	. 2 |- ( ( ( ps /\ ch /\ th ) /\ ta /\ et ) -> ze )
8	4, 5, 6, 7	syl3anc 1185	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ w3a 937

This theorem is referenced by:  syl312anc  1206  syl321anc  1207  syl313anc  1209  syl331anc  1210  pythagtrip  13239  nmolb2d  18783  nmoleub  18796  cvlcvr1  30235  4atlem12b  30506  dalawlem10  30775  dalawlem13  30778  dalawlem15  30780  osumcllem11N  30861  lhp2atne  30929  lhp2at0ne  30931  cdlemd  31102  ltrneq3  31103  cdleme7d  31141  cdlemeg49le  31406  cdleme  31455  cdlemg1a  31465  ltrniotavalbN  31479  cdlemg44  31628  cdlemk19  31764  cdlemk27-3  31802  cdlemk33N  31804  cdlemk34  31805  cdlemk49  31846  cdlemk53a  31850  cdlemk19u  31865  cdlemk56w  31868  dia2dimlem4  31963  dih1dimatlem0  32224

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 179  df-an 362  df-3an 939