Theorem syl221anc 1241

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 )
syl221anc.6	|- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ et ) -> ze )

Assertion

Ref	Expression
syl221anc	|- ( ph -> ze )

Proof of Theorem syl221anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2 |- ( ph -> ps )
2		sylXanc.2	. 2 |- ( ph -> ch )
3		sylXanc.3	. . 3 |- ( ph -> th )
4		sylXanc.4	. . 3 |- ( ph -> ta )
5	3, 4	jca 530	. 2 |- ( ph -> ( th /\ ta ) )
6		sylXanc.5	. 2 |- ( ph -> et )
7		syl221anc.6	. 2 |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ et ) -> ze )
8	1, 2, 5, 6, 7	syl211anc 1236	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 974

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 185  df-an 369  df-3an 976

This theorem is referenced by:  syl222anc  1246  vtocldf  3107  f1oprswap  5794  dmdcand  10310  modmul12d  11995  modnegd  11996  modadd12d  11997  exprec  12161  splval2  12696  eulerthlem2  14413  fermltl  14415  odzdvds  14423  efgredleme  16977  efgredlemc  16979  blssps  21111  blss  21112  metequiv2  21197  met1stc  21208  met2ndci  21209  metdstri  21539  xlebnum  21649  caubl  21930  divcxp  23254  cxple2a  23266  cxplead  23288  cxplt2d  23293  cxple2d  23294  mulcxpd  23295  ang180  23365  wilthlem2  23616  lgslem4  23847  lgsvalmod  23863  lgsmod  23869  lgsdir2lem4  23874  lgsdirprm  23877  lgsne0  23881  lgseisen  23901  ax5seglem9  24538  xrsmulgzz  27998  heiborlem8  31577  cdlemd4  33200  cdleme15a  33273  cdleme17b  33286  cdleme25a  33353  cdleme25c  33355  cdleme25dN  33356  cdleme26ee  33360  tendococl  33772  tendodi1  33784  tendodi2  33785  cdlemi  33820  tendocan  33824  cdlemk5a  33835  cdlemk5  33836  cdlemk10  33843  cdlemk5u  33861  cdlemkfid1N  33921  pellexlem6  35112  rpexpmord  35226  acongeq  35263  jm2.25  35284  stoweidlem42  37174  stoweidlem51  37183  ldepspr  38565