Theorem syl121anc 1233

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

Hypotheses

Ref	Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
syl121anc.5

Assertion

Ref	Expression
syl121anc

Proof of Theorem syl121anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. 2
2		sylXanc.2	. . 3
3		sylXanc.3	. . 3
4	2, 3	jca 532	. 2
5		sylXanc.4	. 2
6		syl121anc.5	. 2
7	1, 4, 5, 6	syl3anc 1228	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  syl122anc  1237  disjxiun  4449  fsnunf2  6110  tfisi  6693  fnsuppeq0  6947  axdc4lem  8856  div32d  10368  div13d  10369  expdivd  12324  pcqmul  14377  pcid  14396  pcneg  14397  pc2dvds  14402  pcz  14404  pcaddlem  14407  pcadd  14408  pcmpt2  14412  pcbc  14419  qexpz  14420  expnprm  14421  sylow1lem1  16618  lspsneleq  17761  lspsneq  17768  lspfixed  17774  frlmsslss2  18805  chmatval  19330  chpmat1dlem  19336  chpdmatlem2  19340  ucncn  20788  ucnextcn  20807  ssblex  20931  prdsxmslem2  21032  voliunlem1  21960  deg1mul3le  22517  deg1pw  22521  fta1blem  22569  bcmono  23552  dchrisum0flblem1  23693  dchrisum0flblem2  23694  pntibndlem1  23774  pntlemr  23787  0wlkon  24549  0pthon  24581  clwlkfclwwlk  24844  nv1  25579  resf1o  27553  omndmul3  27703  rngurd  27778  measun  28182  measvuni  28185  measunl  28187  btwnconn1lem14  29750  segcon2  29755  seglelin  29766  neibastop3  30180  upixp  30220  fdc  30238  eldioph2b  30696  jm2.19lem4  30934  jm2.19  30935  jm2.26a  30942  jm2.26  30944  hbtlem2  31073  fnchoice  31404  stoweidlem42  31824  stoweidlem59  31841  fourierdlem42  31931  eqlkr3  34826  lkrshp  34830  lfl1dim  34846  lfl1dim2N  34847  eqlkr4  34890  2llnneN  35133  3dim2  35192  4atlem3  35320  4atlem11  35333  4atlem12  35336  pexmidlem4N  35697  lhp2at0nle  35759  lhple  35766  ltrnideq  35900  cdlemd9  35931  cdleme0ex2N  35949  cdleme0moN  35950  cdleme11a  35985  cdleme30a  36104  cdlemefs32sn1aw  36140  cdleme43fsv1snlem  36146  cdlemefs31fv1  36150  cdlemefs45eN  36157  cdleme41sn3a  36159  cdleme35h  36182  cdleme36a  36186  cdleme40m  36193  cdleme40n  36194  cdleme41sn3aw  36200  cdleme42h  36208  cdleme42k  36210  cdleme42mN  36213  cdleme43cN  36217  cdleme17d3  36222  cdleme48fvg  36226  cdlemeg47rv2  36236  cdlemeg46c  36239  cdlemeg46sfg  36246  cdlemeg46rjgN  36248  cdlemeg46rgv  36254  cdlemeg46req  36255  cdlemeg46gfv  36256  cdlemeg46gfre  36258  cdlemeg49lebilem  36265  cdleme50trn2  36277  cdlemg2kq  36328  cdlemb3  36332  cdlemg4f  36341  cdlemg9a  36358  cdlemg9b  36359  cdlemg9  36360  cdlemg11aq  36364  cdlemg12a  36369  cdlemg12b  36370  cdlemg12c  36371  cdlemg12d  36372  cdlemg12f  36374  cdlemg12g  36375  cdlemg12  36376  cdlemg13a  36377  cdlemg16  36383  cdlemg17e  36391  cdlemg17f  36392  cdlemg17g  36393  cdlemg17ir  36396  cdlemg17  36403  cdlemg18b  36405  cdlemg18c  36406  cdlemg33e  36436  trlcoabs2N  36448  trlcocnvat  36450  trlcolem  36452  trlco  36453  cdlemg44  36459  cdlemg47  36462  ltrncom  36464  tendococl  36498  tendoplcl  36507  tendoplcom  36508  tendoplass  36509  tendodi1  36510  tendodi2  36511  tendo0pl  36517  tendoipl  36523  cdlemh1  36541  cdlemi2  36545  tendo0mul  36552  tendo0mulr  36553  cdlemk2  36558  cdlemk3  36559  cdlemk4  36560  cdlemk6  36563  cdlemk8  36564  cdlemk12  36576  cdlemkole  36579  cdlemk14  36580  cdlemk15  36581  cdlemk5u  36587  cdlemk6u  36588  cdlemk12u  36598  cdlemkfid1N  36647  cdlemk19x  36669  cdlemk48  36676  cdlemk53a  36681  cdlemk56  36697  cdleml2N  36703  cdleml3N  36704  cdleml6  36707  cdleml7  36708  dva1dim  36711  dia2dimlem4  36794  dvhlveclem  36835  doca2N  36853  djajN  36864  cdlemn2a  36923  cdlemn3  36924  dihordlem6  36940  dihord5apre  36989  dihglbcpreN  37027  dihmeetcN  37029  dihmeetbN  37030  dihmeetlem10N  37043  dihmeetlem12N  37045  dihmeetlem15N  37048  dihmeetALTN  37054  dih1dimatlem0  37055  dihjatcclem3  37147  dihjatcclem4  37148  mapdpglem22  37420  hdmap14lem1a  37596

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 371  df-3an 975