Theorem syl311anc 1198

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 1134	. 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 1184	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ w3a 936

This theorem is referenced by:  syl312anc  1205  syl321anc  1206  syl313anc  1208  syl331anc  1209  pythagtrip  13167  nmolb2d  18709  nmoleub  18722  cvlcvr1  29826  4atlem12b  30097  dalawlem10  30366  dalawlem13  30369  dalawlem15  30371  osumcllem11N  30452  lhp2atne  30520  lhp2at0ne  30522  cdlemd  30693  ltrneq3  30694  cdleme7d  30732  cdlemeg49le  30997  cdleme  31046  cdlemg1a  31056  ltrniotavalbN  31070  cdlemg44  31219  cdlemk19  31355  cdlemk27-3  31393  cdlemk33N  31395  cdlemk34  31396  cdlemk49  31437  cdlemk53a  31441  cdlemk19u  31456  cdlemk56w  31459  dia2dimlem4  31554  dih1dimatlem0  31815

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938