Theorem syl221anc 1279

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 535	. 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 1274	1 |- ( ph -> ze )

Syntax hints:   -> wi 4   /\ wa 371   /\ w3a 985

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 189  df-an 373  df-3an 987

This theorem is referenced by:  syl222anc  1284  vtocldf  3097  f1oprswap  5854  dmdcand  10412  modmul12d  12144  modnegd  12145  modadd12d  12146  exprec  12313  splval2  12864  eulerthlem2  14730  fermltl  14732  odzdvds  14740  odzdvdsOLD  14746  efgredleme  17393  efgredlemc  17395  blssps  21439  blss  21440  metequiv2  21525  met1stc  21536  met2ndci  21537  metdstri  21868  metdstriOLD  21883  xlebnum  21996  caubl  22277  divcxp  23632  cxple2a  23644  cxplead  23666  cxplt2d  23671  cxple2d  23672  mulcxpd  23673  ang180  23743  wilthlem2  23994  lgslem4  24227  lgsvalmod  24243  lgsmod  24249  lgsdir2lem4  24254  lgsdirprm  24257  lgsne0  24261  lgseisen  24281  ax5seglem9  24967  xrsmulgzz  28440  heiborlem8  32150  cdlemd4  33767  cdleme15a  33840  cdleme17b  33853  cdleme25a  33920  cdleme25c  33922  cdleme25dN  33923  cdleme26ee  33927  tendococl  34339  tendodi1  34351  tendodi2  34352  cdlemi  34387  tendocan  34391  cdlemk5a  34402  cdlemk5  34403  cdlemk10  34410  cdlemk5u  34428  cdlemkfid1N  34488  pellexlem6  35678  rpexpmord  35796  acongeq  35833  jm2.25  35854  stoweidlem42  37903  stoweidlem51  37912  ldepspr  40319