Theorem syl22anc 844

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

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl22anc.5	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl22anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl22anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 516	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 842	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  preqsnd  4790  fr2nr  5595  soltmin  6086  f1oprg  6813  f1prex  7228  fveqf1o  7246  weniso  7298  fr3nr  7715  suppofssd  8143  smogt  8297  smocdmdom  8298  oacomf1o  8490  en2prd  8984  difsnen  8987  enfixsn  9014  domss2  9064  ssenen  9079  marypha1lem  9336  fisupcl  9373  ordtypelem3  9425  ordtypelem8  9430  oieu  9444  oismo  9445  wofib  9450  wemaplem2  9452  wemapso  9456  wemapso2lem  9457  unxpwdom2  9493  infdifsn  9569  oemapvali  9596  cantnflem1c  9599  cantnflem1  9601  cantnf  9605  cnfcom3  9616  r1ordg  9693  dif1card  9923  infxpenlem  9926  dfac8clem  9945  infxp  10127  infmap2  10130  cflim2  10176  coftr  10186  fin2i2  10231  enfin2i  10234  fin23lem26  10238  fin23lem27  10241  fin23lem40  10264  isf32lem2  10267  isf32lem3  10268  isf32lem4  10269  isf32lem7  10272  isf32lem9  10274  fin1a2lem13  10325  fin12  10326  alephexp1  10493  gchdomtri  10543  fpwwe2lem11  10555  fpwwe2lem12  10556  gchpwdom  10584  gchhar  10593  adderpqlem  10868  mulerpqlem  10869  addassnq  10872  mulassnq  10873  distrnq  10875  mulidnq  10877  recmulnq  10878  ltexnq  10889  distrlem1pr  10939  distrlem4pr  10940  prlem936  10961  reclem3pr  10963  mulcmpblnr  10985  mulgt0d  11292  mul4d  11349  add4d  11366  add42d  11367  subcan  11440  addsub4d  11543  subadd4d  11544  sub4d  11545  2addsubd  11546  addsubeq4d  11547  muladdd  11599  mulsubd  11600  addgegt0d  11714  addgtge0d  11715  addge0d  11717  mulge0d  11718  le2subd  11761  ltleaddd  11762  leltaddd  11763  lt2subd  11765  divdivdiv  11847  divcan5  11848  divne0d  11938  recdivd  11939  recdiv2d  11940  divcan6d  11941  ddcand  11942  rec11d  11943  divmuldivd  11963  divmul13d  11964  divmul24d  11965  divadddivd  11966  divsubdivd  11967  divmuleqd  11968  divdivdivd  11969  mulge0b  12017  recreclt  12046  divgt0d  12082  mulgt1d  12083  lemulge11d  12084  lemulge12d  12085  ltmul12ad  12088  lemul12ad  12089  lemul12bd  12090  supmul1  12116  nndivtr  12215  qreccl  12910  ledivdivd  13002  lediv12ad  13036  lt2mul2divd  13046  xlt2add  13203  supxrun  13259  supxrre  13270  infxrre  13280  elicore  13342  iccss2  13361  iccssico2  13364  icossico2d  13365  lincmb01cmp  13439  iccf1o  13440  nnge2recico01  13451  fzrev2i  13534  2tnp1ge0ge0  13779  m1modnnsub1  13870  modaddmodup  13887  modaddmodlo  13888  modsubdir  13893  fzennn  13921  sermono  13987  mulexpz  14055  expaddz  14059  sqdiv  14074  expsubd  14110  ltexp2a  14119  expmordi  14120  leexp2a  14125  expmulnbnd  14188  digit1  14190  lt2sqd  14209  le2sqd  14210  sq11d  14211  bcm1k  14268  bcp1n  14269  bcp1nk  14270  hashf1lem1  14408  cshw1  14775  2swrd2eqwrdeq  14906  ofccat  14922  absrele  15261  sqreulem  15313  sqrtmuld  15378  sqrtsq2d  15379  sqrtled  15380  sqrtltd  15381  sqr11d  15382  abs3lemd  15417  rlimuni  15503  climuni  15505  lo1resb  15517  o1resb  15519  2clim  15525  addcn2  15547  mulcn2  15549  o1of2  15566  o1rlimmul  15572  lo1add  15580  lo1mul  15581  isercolllem1  15618  caucvgrlem  15626  iseraltlem2  15636  iseraltlem3  15637  mptfzshft  15731  fsumrev  15732  fsum0diag2  15736  binomlem  15785  climcndslem1  15805  climcndslem2  15806  harmonic  15815  mertenslem1  15840  fprodser  15905  fprodrev  15933  efcllem  16033  moddvds  16223  dvds1  16279  dvdsext  16281  evennn2n  16311  bitsinv1  16402  sadaddlem  16426  sadasslem  16430  sadeq  16432  mulgcd  16508  dvdssqlem  16526  lcmftp  16596  rpmulgcd2  16616  coprmproddvdslem  16622  isprm5  16668  isprm6  16675  crth  16739  eulerthlem2  16743  prmdiveq  16747  pythagtriplem11  16787  pythagtriplem13  16789  pcgcd1  16839  pcprmpw2  16844  pcaddlem  16850  fldivp1  16859  4sqlem12  16918  4sqlem14  16920  4sqlem15  16921  4sqlem16  16922  vdwapun  16936  mreexexlem4d  17604  acsfn1  17618  acsfn2  17620  sscpwex  17773  rescabs  17791  yonedainv  18238  chnub  18579  subm0  18774  pmtrfb  19431  psgnunilem1  19459  odmodnn0  19506  odeq  19516  dfod2  19530  sylow1lem1  19564  lsmsubg  19620  lsmmod  19641  lsmdisj2  19648  ghmplusg  19812  odadd  19816  gexexlem  19818  lt6abl  19861  cyggex2  19863  dprdfinv  19987  dmdprdsplitlem  20005  dpjidcl  20026  ablfacrp  20034  ablfacrp2  20035  ablfac1c  20039  ablfac1eu  20041  omndadd2d  20096  omndadd2rd  20097  omndmul2  20099  acsfn1p  20771  lcomfsupp  20892  lssvancl1  20935  lssvnegcl  20946  lspprvacl  20989  ellspsni  20991  lspsn  20992  lmhmplusg  21034  lmhmima  21037  lmhmpreima  21038  reslmhm  21042  lbsind2  21071  lsmcl  21073  lsmelval2  21075  lsppreli  21080  lspprabs  21085  pj1lmhm  21090  lssvs0or  21103  lspabs3  21114  lspfixed  21121  lspexch  21122  lsmcv  21134  lspsolv  21136  drngnidl  21236  rhmpreimaidl  21270  rngqiprngimfo  21294  rngqiprngfulem4  21307  gzrngunit  21408  zringlpirlem3  21439  prmirredlem  21447  znf1o  21526  znunithash  21539  freshmansdream  21549  ofldchr  21551  frlmsubgval  21740  frlmvplusgvalc  21742  frlmvscaval  21743  frlmphllem  21755  frlmphl  21756  frlmssuvc1  21769  frlmsslsp  21771  frlmup1  21773  frlmup2  21774  lindfind2  21793  lindfrn  21796  f1lindf  21797  islindf4  21813  mplbas2  22018  evlslem3  22056  evlslem1  22058  evladdval  22079  evlmulval  22080  evlsaddval  22105  evlsmulval  22106  coe1addfv  22251  lply1binom  22296  evl1addd  22327  evl1subd  22328  evl1muld  22329  mamudi  22386  mamudir  22387  1marepvmarrepid  22558  mdetrlin  22585  smadiadetglem1  22654  smadiadetg  22656  cramerimplem1  22666  mat2pmatscmxcl  22723  m2pmfzgsumcl  22731  pmatcollpw  22764  pmatcollpwfi  22765  pmatcollpw3fi1lem1  22769  cpmidpmatlem2  22854  cpmadugsumlemF  22859  chcoeffeqlem  22868  ntrin  23044  topssnei  23107  restbas  23141  restntr  23165  cnntri  23254  fiuncmp  23387  nllyrest  23469  nllyidm  23472  hausllycmp  23477  cldllycmp  23478  hauspwdom  23484  txcld  23586  txcn  23609  txlly  23619  txnlly  23620  txhaus  23630  txlm  23631  txkgen  23635  xkococnlem  23642  cnmpt2res  23660  xkoinjcn  23670  basqtop  23694  qtopeu  23699  trfbas2  23826  neifil  23863  hausflim  23964  alexsubALTlem2  24031  cnextfval  24045  cnextfvval  24048  cnextf  24049  cnextfres  24052  clssubg  24092  utop2nei  24233  utop3cls  24234  utopreg  24235  psmetlecl  24298  xmetlecl  24329  prdsxmetlem  24351  bldisj  24381  imasf1obl  24471  prdsbl  24474  stdbdmet  24499  stdbdmopn  24501  met2ndci  24505  metcnp  24524  metustto  24536  metustexhalf  24539  cfilucfil  24542  metucn  24554  lssnlm  24684  nmotri  24722  nmoid  24725  tgioo  24779  blcvx  24781  xrsmopn  24796  reperflem  24802  reconnlem2  24811  opnreen  24815  metdsge  24833  metdsre  24837  metdscnlem  24839  metnrmlem1a  24842  metnrmlem1  24843  metnrmlem3  24845  cncfmet  24894  cnmpopc  24913  icopnfcnv  24927  icopnfhmeo  24928  cnllycmp  24941  evth  24944  lebnumii  24951  nmoleub2lem3  25100  iscfil2  25251  cfil3i  25254  iscfil3  25258  cfilfcls  25259  iscau3  25263  iscmet3lem2  25277  caubl  25293  lmcau  25298  cssbn  25360  rrxcph  25377  minveclem2  25411  pjthlem1  25422  pjthlem2  25423  ivthicc  25443  ovollecl  25468  ovolunlem1a  25481  ovolunnul  25485  ovoliunlem1  25487  ismbl2  25512  nulmbl2  25521  unmbl  25522  volun  25530  voliunlem2  25536  ioombl1lem2  25544  uniioombllem2a  25567  uniioombllem3  25570  uniioombllem4  25571  dyaddisjlem  25580  dyadmaxlem  25582  opnmbllem  25586  volsup2  25590  volcn  25591  ismbfd  25624  mbfi1fseqlem1  25700  mbfi1fseqlem5  25704  itg2lecl  25723  itg2monolem2  25736  itg2gt0  25745  itgspliticc  25822  ellimc3  25864  limcres  25871  dvfval  25882  dvres3  25898  dvres3a  25899  dvmptresicc  25901  dvnff  25908  dvnadd  25914  dvn2bss  25915  dvnres  25916  dvcmul  25929  dvcmulf  25930  dvmptres3  25941  dvmptres2  25947  dvmptntr  25956  dvexp3  25963  dvferm1lem  25969  dvlip  25978  dvlipcn  25979  dvlip2  25980  c1liplem1  25981  dvgt0lem1  25987  dvgt0lem2  25988  dvne0  25996  lhop1lem  25998  lhop2  26000  lhop  26001  dvcnvrelem1  26002  dvcnvrelem2  26003  dvcvx  26005  dvfsumle  26006  dvfsumabs  26008  dvfsumlem2  26012  ftc1lem6  26026  ftc1  26027  ftc2ditglem  26030  itgsubstlem  26033  itgpowd  26035  tdeglem4  26043  mdegaddle  26057  mdegmullem  26061  ply1rem  26149  fta1glem2  26152  fta1blem  26154  ig1peu  26158  ig1pdvds  26163  dgrmulc  26254  dgrcolem1  26256  plydivlem4  26280  plydiveu  26282  fta1lem  26291  vieta1lem1  26294  vieta1lem2  26295  plyexmo  26297  taylfvallem1  26340  taylfval  26342  tayl0  26345  taylplem1  26346  taylply2  26351  taylply  26352  dvtaylp  26353  dvntaylp  26354  dvntaylp0  26355  taylthlem1  26356  taylthlem2  26357  ulmcaulem  26377  ulmcau  26378  ulmcn  26382  ulmdvlem1  26383  radcnvlem1  26396  radcnvle  26403  psercn  26409  pserdvlem2  26411  pserdv  26412  abelth  26424  tanregt0  26521  dvlog2lem  26634  efopn  26640  logtayllem  26641  logccv  26645  cxplt3  26682  cxpmul2zd  26698  cxpltd  26701  cxpled  26702  cxplt3d  26717  cxple3d  26718  dvsqrt  26724  cxpcn3  26730  cxpaddle  26734  cxpeq  26739  angcan  26784  angvald  26786  ang180lem2  26792  ang180  26796  isosctrlem3  26802  dquartlem1  26833  atantayl2  26920  leibpi  26924  log2tlbnd  26927  birthdaylem3  26935  xrlimcnp  26950  efrlim  26951  o1cxp  26956  jensenlem2  26969  jensen  26970  fsumharmonic  26993  lgamucov  27019  lgamcvg2  27036  wilthlem1  27049  basellem3  27064  basellem6  27067  basellem8  27069  ppisval  27085  chtwordi  27137  ppiwordi  27143  mumullem2  27161  mpodvdsmulf1o  27175  dvdsmulf1o  27177  fsumvma  27194  fsumvma2  27195  chpchtsum  27200  chpub  27201  logfacubnd  27202  dchrmulcl  27230  dchrinv  27242  dchrptlem1  27245  dchrptlem2  27246  sumdchr2  27251  dchr2sum  27254  bposlem7  27271  lgslem1  27278  lgslem3  27280  lgsdirprm  27312  lgsqrlem2  27328  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem4  27359  lgseisen  27360  lgsquadlem1  27361  lgsquad2lem1  27365  lgsquad3  27368  m1lgs  27369  2sqlem7  27405  2sq2  27414  2sqmod  27417  chebbnd1lem2  27451  chebbnd1lem3  27452  rplogsumlem1  27465  rpvmasumlem  27468  dchrvmasumlem1  27476  dchrvmasum2lem  27477  dchrvmasumlema  27481  dchrisum0flblem2  27490  dchrisum0fno1  27492  dchrisum0re  27494  logdivsum  27514  pntrsumbnd2  27548  pntpbnd1a  27566  pntpbnd1  27567  pntibndlem2  27572  pntlemr  27583  pntlemj  27584  pntlemf  27586  pnt2  27594  padicabv  27611  ostth2lem2  27615  lesrecd  27810  ltsrecd  27812  madebday  27910  addsproplem6  27984  negsproplem6  28043  mulsproplem13  28138  mulsproplem14  28139  ltmulsd  28147  mulsgt0d  28155  f1otrg  28957  brbtwn2  28992  colinearalglem2  28994  axcgrtr  29002  axcgrid  29003  axsegconlem7  29010  axsegcon  29014  ax5seglem3  29018  ax5seglem6  29021  ax5seg  29025  axpaschlem  29027  axlowdimlem17  29045  axcontlem2  29052  axcontlem4  29054  axcontlem7  29057  axcontlem8  29058  ecgrtg  29070  usgredg2v  29314  vtxdgoddnumeven  29640  2trlond  30025  eupthp1  30304  nmobndi  30864  ubthlem2  30960  ubthlem3  30961  minvecolem2  30964  shuni  31389  pjhthlem1  31480  chscllem2  31727  pjcompi  31761  mayete3i  31817  unoplin  32009  hmoplin  32031  nmophmi  32120  mdslmd4i  32422  isoun  32794  submuladdd  32832  receqid  32836  xrge0addcld  32854  xrofsup  32859  eliccelico  32869  elicoelioo  32870  difioo  32874  hashpss  32901  sgnmul  32927  rexdiv  33004  mgcmnt1d  33076  mgcmnt2d  33077  xrge0addgt0  33096  cycpmcl  33197  cycpm2tr  33200  cyc3evpm  33231  cycpmconjslem2  33236  fldgensdrg  33398  qusker  33432  eqgvscpbl  33433  ringlsmss1  33479  ringlsmss2  33480  lidlmcld  33502  intlidl  33503  lidlunitel  33506  elrspunidl  33511  idlinsubrg  33514  isprmidlc  33530  rhmpreimaprmidl  33534  qsidomlem1  33535  ssdifidllem  33539  mxidlmaxv  33551  mxidlprm  33553  ssmxidllem  33556  opprmxidlabs  33570  qsdrnglem2  33579  selvply1rhmlem4  33707  mplvrpmmhm  33730  mplvrpmrhm  33731  esplyind  33759  resssra  33771  ply1degltdimlem  33806  lindsunlem  33808  sdrgfldext  33834  fldsdrgfldext  33845  finexttrb  33849  fldgenfldext  33852  fldextrspunlem1  33859  algextdeglem4  33904  algextdeglem8  33908  constrextdg2lem  33932  mdetpmtr2  34008  mdetpmtr12  34009  madjusmdetlem1  34011  madjusmdetlem4  34014  rhmpreimacn  34069  unitdivcld  34085  xrge0mulc1cn  34125  qqhnm  34174  esumcst  34247  esumfsup  34254  esumpmono  34263  esumcvg  34270  difelsiga  34317  sigapisys  34339  sigapildsys  34346  ldgenpisyslem1  34347  1stmbfm  34444  2ndmbfm  34445  dya2icoseg  34461  sibfinima  34523  probmeasb  34614  orvcgteel  34652  orvclteel  34657  ballotlemsima  34700  ballotlemfrceq  34713  ccatmulgnn0dir  34726  fct2relem  34781  ftc2re  34782  chtvalz  34813  r1filimi  35284  subfacp1lem2a  35408  subfaclim  35416  erdsze2lem2  35432  cvmliftlem2  35514  cvmliftlem10  35522  cvmliftlem13  35524  cvmliftiota  35529  cvmlift2lem9  35539  cvmlift2lem11  35541  cvmlift2lem12  35542  cvmliftphtlem  35545  cvmlift3lem6  35552  cvmlift3lem7  35553  cvmlift3lem9  35555  snmlff  35557  mrsubfval  35736  wzel  36050  wsuclem  36051  brsegle  36336  opnregcld  36558  weiunfrlem  36692  fin2so  37974  poimirlem17  38004  poimirlem23  38010  opnmbllem0  38023  mblfinlem3  38026  mblfinlem4  38027  itg2addnclem  38038  itg2addnc  38041  itg2gt0cn  38042  ftc1cnnclem  38058  ftc1cnnc  38059  areacirclem5  38079  indexdom  38101  sstotbnd2  38141  isbnd3  38151  isbnd3b  38152  cntotbnd  38163  ismtyima  38170  heibor1lem  38176  heiborlem8  38185  rrncmslem  38199  reheibor  38206  lkrlsp  39594  lshpkrlem5  39606  ldualssvscl  39650  ldualssvsubcl  39651  llnmlplnN  40031  llncvrlpln  40050  pmapjat1  40345  pclfinN  40392  lautlt  40583  lauteq  40587  lautco  40589  ltrn11  40618  ltrnle  40621  ltrneq2  40640  cdlemednuN  40792  cdleme20k  40811  cdleme20l2  40813  cdleme20l  40814  cdleme20m  40815  cdleme21c  40819  cdleme22e  40836  cdleme22eALTN  40837  cdlemefrs32fva  40892  cdlemg4g  41108  cdlemg18b  41171  cdlemg18c  41172  cdlemj3  41315  dia2dimlem5  41560  dvhopN  41608  cdlemm10N  41610  dihjatcclem4  41913  dochexmidlem2  41953  lclkrlem2o  42013  lcfrlem5  42038  lcfrlem6  42039  lcdlssvscl  42098  mapdpglem6  42170  mapdpglem9  42172  mapdpglem12  42175  mapdpglem14  42177  mapdindp0  42211  hdmaprnlem7N  42347  hdmaprnlem8N  42348  hdmaprnlem3eN  42350  hgmapvvlem3  42417  dvun  42836  addinvcom  42909  mzpsubst  43197  eldioph2lem1  43209  eldioph2lem2  43210  eldioph2b  43212  diophin  43221  irrapxlem2  43268  irrapxlem4  43270  irrapxlem5  43271  pellexlem1  43274  pellexlem2  43275  pellexlem6  43279  elpell1qr2  43317  pell1qrgaplem  43318  pell1qrgap  43319  pellqrex  43324  pellfundex  43331  pellfund14  43343  rmspecsqrtnq  43351  rmxyadd  43366  congsub  43415  mzpcong  43417  congrep  43418  acongtr  43423  acongrep  43425  jm2.19lem1  43434  jm2.22  43440  jm2.23  43441  jm2.26lem3  43446  jm2.26  43447  jm2.27a  43450  fnwe2lem2  43496  aomclem6  43504  hbtlem2  43569  hbtlem4  43571  hbtlem5  43573  dgraa0p  43594  rngunsnply  43614  proot1hash  43640  nnoeomeqom  43757  cantnf2  43770  omabs2  43777  naddcnff  43807  naddcnffo  43809  naddcnfcom  43811  naddcnfid1  43812  expgrowth  44779  fpmd  45707  abslt2sqd  45805  ioondisj2  45938  ioondisj1  45939  eliocre  45954  ioossioobi  45962  iooiinicc  45987  iooiinioc  46001  lptioo2  46076  limcresiooub  46085  limsupequzlem  46165  xlimmnfvlem2  46276  xlimpnfvlem2  46280  cncfuni  46329  cncfiooicclem1  46336  cxpcncf2  46342  dvcnre  46359  dvresntr  46361  dvresioo  46364  dvbdfbdioolem1  46371  dvnmptdivc  46381  dvnxpaek  46385  itgsinexplem1  46397  itgcoscmulx  46412  itgiccshift  46423  itgperiod  46424  ovolsplit  46431  stoweidlem11  46454  stoweidlem26  46469  stoweidlem34  46477  stoweidlem36  46479  stoweidlem38  46481  stirlinglem5  46521  dirkercncflem2  46547  dirkercncflem4  46549  fourierdlem20  46570  fourierdlem58  46607  fourierdlem72  46621  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem79  46628  fourierdlem80  46629  fourierdlem87  46636  fourierdlem94  46643  fourierdlem103  46652  fourierdlem104  46653  fourierdlem107  46656  fourierdlem113  46662  sqwvfoura  46671  sqwvfourb  46672  fourierswlem  46673  fouriersw  46674  etransclem46  46723  etransclem47  46724  rrndistlt  46733  rrnprjdstle  46744  ioorrnopnxrlem  46749  sge0ssre  46840  sge0seq  46889  hsphoidmvle2  47028  hsphoidmvle  47029  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmv1lelem3  47036  hoidmvlelem1  47038  hoidifhspdmvle  47063  hoiqssbllem2  47066  ovolval5lem2  47096  iinhoiicc  47117  iunhoiioo  47119  vonioolem2  47124  vonicclem2  47127  issmflem  47170  submodlt  47819  iccpartdisj  47912  m1expevenALTV  48138  fpprel2  48232  tgoldbach  48308  opstrgric  48417  gpg3kgrtriex  48580  nn0eo  49019  fdivpm  49034  refdivpm  49035  elbigolo1  49048  logbpw2m1  49058  fllog2  49059  dignn0flhalflem1  49106  dignn0flhalflem2  49107  itsclinecirc0in  49266  2itscplem2  49270  itscnhlinecirc02plem1  49273  iccdisj2  49387