Theorem syl112anc 1232

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

Hypotheses

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

Assertion

Ref	Expression
syl112anc

Proof of Theorem syl112anc

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

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

This theorem is referenced by:  rmob2  3432  fveqf1o  6205  enfixsn  7646  gruina  9217  grur1  9219  enqeq  9333  recrec  10266  rec11r  10268  divdivdiv  10270  dmdcan  10279  ddcan  10283  rereccl  10287  div2neg  10292  divmuld  10367  divmul2d  10378  divmul3d  10379  divassd  10380  div12d  10381  div23d  10382  divdird  10383  divsubdird  10384  div11d  10385  ltmul12a  10423  ltdiv1  10431  ltrec  10451  lt2msq1  10453  lediv2  10460  supmul1  10533  qbtwnre  11427  xlemul1a  11509  xlemul1  11511  xadd4d  11524  quoremz  11982  quoremnn0ALT  11984  expgt1  12204  nnlesq  12271  expnbnd  12295  expmulnbnd  12298  discr1  12302  facubnd  12378  hashf1lem1  12504  2swrdeqwrdeq  12678  sqrlem6  13081  mulcn2  13418  climcnds  13663  geomulcvg  13685  cvgrat  13692  eftlub  13844  eflegeo  13856  tanhlt1  13895  sin01bnd  13920  cos01bnd  13921  eirrlem  13937  bitsmod  14086  mulgcd  14184  prmind2  14228  mulgcddvds  14245  qnumgt0  14283  iserodd  14359  pcpremul  14367  fldivp1  14416  pcfaclem  14417  qexpz  14420  prmpwdvds  14422  pockthg  14424  prmreclem1  14434  prmreclem5  14438  4sqlem10  14465  4sqlem12  14474  4sqlem16  14478  4sqlem17  14479  vdwlem3  14501  vdwlem8  14506  vdwlem9  14507  0ram  14538  ramz2  14542  xpsc0  14957  xpsc1  14958  odmulg  16578  dfod2  16586  odf1o1  16592  odf1o2  16593  sylow3lem4  16650  ablsub4  16823  odadd1  16854  odadd2  16855  ablfacrp2  17118  ablfac1b  17121  ablfac1eu  17124  pgpfac1lem3a  17127  pgpfaclem2  17133  chrcong  18566  znrrg  18604  cygznlem1  18605  chpdmatlem3  19341  txdis  20133  txdis1cn  20136  ptunhmeo  20309  qustgplem  20619  blcld  21008  nlmvscnlem2  21194  blcvx  21303  metds0  21354  metdseq0  21358  icopnfcnv  21442  lebnumii  21466  ipcau2  21677  tchcphlem1  21678  ipcnlem2  21684  csbren  21826  trirn  21827  dyadf  22000  dyadovol  22002  dyaddisjlem  22004  dyadmaxlem  22006  opnmbllem  22010  mbfmulc2lem  22054  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1fseqlem6  22127  itg2mulclem  22153  itg2monolem1  22157  itg2monolem3  22159  itg2cnlem2  22169  itgabs  22241  dvlip  22394  dvlt0  22406  dvcvx  22421  ftc1lem4  22440  dgrcolem2  22671  aaliou3lem2  22739  aaliou3lem9  22746  itgulm  22803  radcnvlem1  22808  abelthlem2  22827  abelthlem7  22833  tangtx  22898  cosne0  22917  cosordlem  22918  tanord1  22924  logdivlti  23005  logcnlem4  23026  logf1o2  23031  cxpcn3lem  23121  cxpaddle  23126  ang180lem2  23142  atanlogsublem  23246  atantan  23254  atanbndlem  23256  atans2  23262  leibpi  23273  log2tlbnd  23276  birthdaylem3  23283  efrlim  23299  jensenlem2  23317  ftalem1  23346  ftalem5  23350  basellem1  23354  basellem4  23357  fsumdvdsdiaglem  23459  dvdsflf1o  23463  fsumfldivdiaglem  23465  ppiub  23479  mersenne  23502  dchrptlem1  23539  bposlem1  23559  bposlem2  23560  bposlem4  23562  lgsdilem  23597  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem3  23626  lgsquadlem1  23629  lgsquadlem2  23630  2sqlem3  23641  2sqlem8  23647  2sqlem11  23650  2sqblem  23652  chebbnd1lem2  23655  chebbnd1lem3  23656  rplogsumlem1  23669  rplogsumlem2  23670  dchrisumlem1  23674  dchrmusum2  23679  dchrisum0flblem1  23693  mulog2sumlem1  23719  logdivbnd  23741  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntlemh  23784  pntlemr  23787  pntlemk  23791  pntlemo  23792  ostth2lem1  23803  ostth2lem2  23819  ostth2lem3  23820  ostth3  23823  legov  23972  axsegcon  24230  axpaschlem  24243  clwwlkf1  24796  vdgrun  24901  vdgrfiun  24902  eupath2lem3  24979  gxmodid  25281  nmbdoplbi  26943  nmcoplbi  26947  nmophmi  26950  nmbdfnlbi  26968  nmcfnlbi  26971  cnlnadjlem7  26992  nmopcoi  27014  resf1o  27553  xdivrec  27623  txomap  27837  unitdivcld  27883  measvunilem  28183  measvuni  28185  measssd  28186  measiuns  28188  measinblem  28191  measdivcst  28196  sibfof  28282  oddpwdc  28293  sseqfv1  28328  sseqfv2  28333  probun  28358  totprobd  28365  dstrvprob  28410  zetacvg  28557  subfaclim  28632  conpcon  28680  cvmliftlem2  28731  cvmliftlem6  28735  cvmliftlem7  28736  cvmliftlem8  28737  cvmliftlem9  28738  cvmliftlem10  28739  snmlff  28774  lineext  29726  hilbert1.1  29804  opnmbllem0  30050  ismblfin  30055  itgabsnc  30084  ftc1cnnclem  30088  nn0prpwlem  30140  bfplem1  30318  bfp  30320  eldioph2lem1  30693  fphpdo  30751  irrapxlem1  30758  irrapxlem2  30759  irrapxlem3  30760  irrapxlem5  30762  pellexlem2  30766  pell1234qrreccl  30790  pell1234qrmulcl  30791  pell1234qrdich  30797  pell1qr1  30807  pellqrexplicit  30813  pellfundex  30822  reglogltb  30827  reglogleb  30828  pellfund14  30834  rmspecsqrtnq  30842  rmxycomplete  30853  jm2.24nn  30897  jm2.17b  30899  jm2.17c  30900  jm2.18  30930  jm2.19lem2  30932  jm2.20nn  30939  jm2.16nn0  30946  jm3.1lem2  30960  areaquad  31184  stoweidlem1  31783  stoweidlem11  31793  stoweidlem14  31796  stoweidlem26  31808  stoweidlem34  31816  stoweidlem38  31820  stoweidlem60  31842  fourierdlem52  31941  etransclem38  32055  domnmsuppn0  32962  lincvalpr  33019  ldepspr  33074  islindeps2  33084  lfl1  34795  lfladdcl  34796  eqlkr  34824  lkrlsp  34827  atcvrj2b  35156  3dim1  35191  3dim2  35192  llni2  35236  2llnjaN  35290  lvoli3  35301  lvoli2  35305  lncvrelatN  35505  lhpat4N  35768  lhpat3  35770  4atexlemex6  35798  ldilco  35840  ltrnid  35859  ltrnatb  35861  ltrnel  35863  ltrncnvel  35866  ltrncnv  35870  ltrn11at  35871  ltrneq  35873  ltrnmwOLD  35876  trlat  35894  trlator0  35896  ltrnnidn  35899  trlid0  35901  trlnidatb  35902  trlnle  35911  trlval3  35912  trlval4  35913  cdlemc2  35917  cdlemc5  35920  cdlemc6  35921  cdlemc  35922  cdlemd2  35924  cdlemd9  35931  cdleme0e  35942  cdleme02N  35947  cdleme0ex1N  35948  cdleme3e  35957  cdleme3g  35959  cdleme3h  35960  cdleme3  35962  cdleme7aa  35967  cdleme7b  35969  cdleme7c  35970  cdleme7d  35971  cdleme7e  35972  cdleme7ga  35973  cdleme7  35974  cdleme9  35978  cdleme16aN  35984  cdleme11c  35986  cdleme11dN  35987  cdleme11e  35988  cdleme11h  35991  cdleme11j  35992  cdleme11k  35993  cdleme12  35996  cdleme21j  36062  cdleme26eALTN  36087  cdleme26f  36089  cdleme26f2  36091  cdlemefrs29bpre0  36122  cdleme35a  36174  cdleme35b  36176  cdleme35c  36177  cdleme35f  36180  cdleme36a  36186  cdleme38m  36189  cdlemeg46rgv  36254  cdlemeg46req  36255  cdlemf  36289  cdlemg2fvlem  36320  cdlemg2l  36329  cdlemg7N  36352  cdlemg12g  36375  cdlemg15  36382  cdlemg17h  36394  cdlemg17  36403  cdlemg19a  36409  cdlemg24  36414  cdlemg37  36415  cdlemg27a  36418  cdlemg31b0N  36420  cdlemg27b  36422  cdlemg31c  36425  cdlemg31d  36426  cdlemg35  36439  trljco  36466  tgrpgrplem  36475  cdlemh2  36542  tendoconid  36555  tendotr  36556  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk53b  36682  cdlemk53  36683  cdlemk54  36684  cdleml3N  36704  cdleml5N  36706  tendospcanN  36750  diclss  36920  dihvalcq2  36974  dihord4  36985  dihord5b  36986  dihord5apre  36989  dihmeetlem1N  37017  dihmeetbclemN  37031  dihmeetlem20N  37053  dihmeetALTN  37054  dihatlat  37061  dihatexv  37065  dochkr1  37205  dochkr1OLDN  37206  lcfl7lem  37226  lclkrlem2m  37246  hdmaplna1  37637  hdmaplns1  37638  hdmaplnm1  37639  lemuldiv3d  37989  lemuldiv4d  37990

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