Theorem syl22anc 851

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 520	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 849	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  preqsnd  4828  fr2nr  5639  soltmin  6137  f1oprg  6868  f1prex  7283  fveqf1o  7301  weniso  7353  fr3nr  7770  suppofssd  8198  smogt  8353  smocdmdom  8354  oacomf1o  8549  en2prd  9043  difsnen  9046  enfixsn  9073  domss2  9123  ssenen  9138  marypha1lem  9392  fisupcl  9429  ordtypelem3  9481  ordtypelem8  9486  oieu  9500  oismo  9501  wofib  9506  wemaplem2  9508  wemapso  9512  wemapso2lem  9513  unxpwdom2  9549  infdifsn  9625  oemapvali  9652  cantnflem1c  9655  cantnflem1  9657  cantnf  9661  cnfcom3  9672  r1ordg  9749  dif1card  9993  infxpenlem  9996  dfac8clem  10015  infxp  10196  infmap2  10199  cflim2  10246  coftr  10256  fin2i2  10301  enfin2i  10304  fin23lem26  10308  fin23lem27  10311  fin23lem40  10334  isf32lem2  10337  isf32lem3  10338  isf32lem4  10339  isf32lem7  10342  isf32lem9  10344  fin1a2lem13  10395  fin12  10396  alephexp1  10563  gchdomtri  10613  fpwwe2lem11  10625  fpwwe2lem12  10626  gchpwdom  10654  gchhar  10663  adderpqlem  10938  mulerpqlem  10939  addassnq  10942  mulassnq  10943  distrnq  10945  mulidnq  10947  recmulnq  10948  ltexnq  10959  distrlem1pr  11009  distrlem4pr  11010  prlem936  11031  reclem3pr  11033  mulcmpblnr  11055  mulgt0d  11364  mul4d  11421  add4d  11438  add42d  11439  subcan  11512  addsub4d  11615  subadd4d  11616  sub4d  11617  2addsubd  11618  addsubeq4d  11619  muladdd  11671  mulsubd  11672  addgegt0d  11786  addgtge0d  11787  addge0d  11789  mulge0d  11790  le2subd  11833  ltleaddd  11834  leltaddd  11835  lt2subd  11837  divdivdiv  11915  divcan5  11916  divne0d  12006  recdivd  12007  recdiv2d  12008  divcan6d  12009  ddcand  12010  rec11d  12011  divmuldivd  12031  divmul13d  12032  divmul24d  12033  divadddivd  12034  divsubdivd  12035  divmuleqd  12036  divdivdivd  12037  mulge0b  12084  recreclt  12113  divgt0d  12149  mulgt1d  12150  lemulge11d  12151  lemulge12d  12152  ltmul12ad  12155  lemul12ad  12156  lemul12bd  12157  supmul1  12183  nndivtr  12282  qreccl  12992  ledivdivd  13084  lediv12ad  13118  lt2mul2divd  13128  xlt2add  13285  supxrun  13341  supxrre  13352  infxrre  13362  elicore  13424  iccss2  13443  iccssico2  13446  icossico2d  13447  lincmb01cmp  13521  iccf1o  13522  nnge2recico01  13533  fzrev2i  13616  2tnp1ge0ge0  13861  m1modnnsub1  13952  modaddmodup  13969  modaddmodlo  13970  modsubdir  13975  fzennn  14003  sermono  14069  mulexpz  14137  expaddz  14141  sqdiv  14156  expsubd  14192  ltexp2a  14201  expmordi  14202  leexp2a  14207  expmulnbnd  14270  digit1  14272  lt2sqd  14291  le2sqd  14292  sq11d  14293  bcm1k  14350  bcp1n  14351  bcp1nk  14352  hashpss  14445  hashf1lem1  14491  cshw1  14858  2swrd2eqwrdeq  14989  ofccat  15005  sgnmul  15143  absrele  15358  sqreulem  15410  sqrtmuld  15475  sqrtsq2d  15476  sqrtled  15477  sqrtltd  15478  sqr11d  15479  abs3lemd  15514  rlimuni  15600  climuni  15602  lo1resb  15614  o1resb  15616  2clim  15622  addcn2  15644  mulcn2  15646  o1of2  15663  o1rlimmul  15669  lo1add  15677  lo1mul  15678  isercolllem1  15715  caucvgrlem  15723  iseraltlem2  15733  iseraltlem3  15734  mptfzshft  15828  fsumrev  15829  fsum0diag2  15833  binomlem  15882  climcndslem1  15902  climcndslem2  15903  harmonic  15912  mertenslem1  15937  fprodser  16002  fprodrev  16030  efcllem  16130  moddvds  16320  dvds1  16376  dvdsext  16378  evennn2n  16408  bitsinv1  16499  sadaddlem  16523  sadasslem  16527  sadeq  16529  mulgcd  16605  dvdssqlem  16623  lcmftp  16693  rpmulgcd2  16713  coprmproddvdslem  16719  isprm5  16765  isprm6  16772  crth  16836  eulerthlem2  16840  prmdiveq  16844  pythagtriplem11  16884  pythagtriplem13  16886  pcgcd1  16936  pcprmpw2  16941  pcaddlem  16947  fldivp1  16956  4sqlem12  17015  4sqlem14  17017  4sqlem15  17018  4sqlem16  17019  vdwapun  17033  mreexexlem4d  17702  acsfn1  17716  acsfn2  17718  sscpwex  17871  rescabs  17889  yonedainv  18336  chnub  18677  subm0  18873  pmtrfb  19534  psgnunilem1  19562  odmodnn0  19609  odeq  19619  dfod2  19633  sylow1lem1  19667  lsmsubg  19723  lsmmod  19744  lsmdisj2  19751  ghmplusg  19915  odadd  19919  gexexlem  19921  lt6abl  19964  cyggex2  19966  dprdfinv  20090  dmdprdsplitlem  20108  dpjidcl  20129  ablfacrp  20137  ablfacrp2  20138  ablfac1c  20142  ablfac1eu  20144  omndadd2d  20199  omndadd2rd  20200  omndmul2  20202  acsfn1p  20879  lcomfsupp  21000  lssvancl1  21043  lssvnegcl  21054  lspprvacl  21097  ellspsni  21099  lspsn  21100  lmhmplusg  21142  lmhmima  21145  lmhmpreima  21146  reslmhm  21150  lbsind2  21179  lsmcl  21181  lsmelval2  21183  lsppreli  21188  lspprabs  21193  pj1lmhm  21198  lssvs0or  21211  lspabs3  21222  lspfixed  21229  lspexch  21230  lsmcv  21242  lspsolv  21244  lidlmcld  21329  drngnidl  21350  rhmpreimaidl  21386  rngqiprngimfo  21411  rngqiprngfulem4  21424  isprmidlc  21442  rhmpreimaprmidl  21447  qsidomlem1  21448  ssdifidllem  21452  gzrngunit  21551  zringlpirlem3  21582  prmirredlem  21590  znf1o  21669  znunithash  21682  freshmansdream  21692  ofldchr  21694  frlmsubgval  21883  frlmvplusgvalc  21885  frlmvscaval  21886  frlmphllem  21898  frlmphl  21899  frlmssuvc1  21912  frlmsslsp  21914  frlmup1  21916  frlmup2  21917  lindfind2  21936  lindfrn  21939  f1lindf  21940  islindf4  21956  mplbas2  22161  evlslem3  22199  evlslem1  22201  evladdval  22222  evlmulval  22223  evlsaddval  22248  evlsmulval  22249  coe1addfv  22394  lply1binom  22438  evl1addd  22469  evl1subd  22470  evl1muld  22471  mamudi  22528  mamudir  22529  1marepvmarrepid  22700  mdetrlin  22727  smadiadetglem1  22796  smadiadetg  22798  cramerimplem1  22808  mat2pmatscmxcl  22865  m2pmfzgsumcl  22873  pmatcollpw  22906  pmatcollpwfi  22907  pmatcollpw3fi1lem1  22911  cpmidpmatlem2  22996  cpmadugsumlemF  23001  chcoeffeqlem  23010  ntrin  23186  topssnei  23249  restbas  23283  restntr  23307  cnntri  23396  fiuncmp  23529  nllyrest  23611  nllyidm  23614  hausllycmp  23619  cldllycmp  23620  hauspwdom  23626  txcld  23728  txcn  23751  txlly  23761  txnlly  23762  txhaus  23772  txlm  23773  txkgen  23777  xkococnlem  23784  cnmpt2res  23802  xkoinjcn  23812  basqtop  23836  qtopeu  23841  trfbas2  23968  neifil  24005  hausflim  24106  alexsubALTlem2  24173  cnextfval  24187  cnextfvval  24190  cnextf  24191  cnextfres  24194  clssubg  24234  utop2nei  24375  utop3cls  24376  utopreg  24377  psmetlecl  24440  xmetlecl  24471  prdsxmetlem  24493  bldisj  24523  imasf1obl  24613  prdsbl  24616  stdbdmet  24641  stdbdmopn  24643  met2ndci  24647  metcnp  24666  metustto  24678  metustexhalf  24681  cfilucfil  24684  metucn  24696  lssnlm  24826  nmotri  24864  nmoid  24867  tgioo  24921  blcvx  24923  xrsmopn  24938  reperflem  24944  reconnlem2  24953  opnreen  24957  metdsge  24975  metdsre  24979  metdscnlem  24981  metnrmlem1a  24984  metnrmlem1  24985  metnrmlem3  24987  cncfmet  25036  cnmpopc  25055  icopnfcnv  25069  icopnfhmeo  25070  cnllycmp  25083  evth  25086  lebnumii  25093  nmoleub2lem3  25242  iscfil2  25393  cfil3i  25396  iscfil3  25400  cfilfcls  25401  iscau3  25405  iscmet3lem2  25419  caubl  25435  lmcau  25440  cssbn  25502  rrxcph  25519  minveclem2  25553  pjthlem1  25564  pjthlem2  25565  ivthicc  25585  ovollecl  25610  ovolunlem1a  25623  ovolunnul  25627  ovoliunlem1  25629  ismbl2  25654  nulmbl2  25663  unmbl  25664  volun  25672  voliunlem2  25678  ioombl1lem2  25686  uniioombllem2a  25709  uniioombllem3  25712  uniioombllem4  25713  dyaddisjlem  25722  dyadmaxlem  25724  opnmbllem  25728  volsup2  25732  volcn  25733  ismbfd  25766  mbfi1fseqlem1  25842  mbfi1fseqlem5  25846  itg2lecl  25865  itg2monolem2  25878  itg2gt0  25887  itgspliticc  25964  ellimc3  26006  limcres  26013  dvfval  26024  dvres3  26040  dvres3a  26041  dvmptresicc  26043  dvnff  26050  dvnadd  26056  dvn2bss  26057  dvnres  26058  dvcmul  26071  dvcmulf  26072  dvmptres3  26083  dvmptres2  26089  dvmptntr  26098  dvexp3  26105  dvferm1lem  26111  dvlip  26120  dvlipcn  26121  dvlip2  26122  c1liplem1  26123  dvgt0lem1  26129  dvgt0lem2  26130  dvne0  26138  lhop1lem  26140  lhop2  26142  lhop  26143  dvcnvrelem1  26144  dvcnvrelem2  26145  dvcvx  26147  dvfsumle  26148  dvfsumabs  26150  dvfsumlem2  26154  ftc1lem6  26168  ftc1  26169  ftc2ditglem  26172  itgsubstlem  26175  itgpowd  26177  tdeglem4  26185  mdegaddle  26199  mdegmullem  26203  ply1rem  26291  fta1glem2  26294  fta1blem  26296  ig1peu  26300  ig1pdvds  26305  dgrmulc  26396  dgrcolem1  26398  plydivlem4  26425  plydiveu  26427  fta1lem  26436  vieta1lem1  26439  vieta1lem2  26440  plyexmo  26442  taylfvallem1  26485  taylfval  26487  tayl0  26490  taylplem1  26491  taylply2  26496  taylply  26497  dvtaylp  26498  dvntaylp  26499  dvntaylp0  26500  taylthlem1  26501  taylthlem2  26502  ulmcaulem  26522  ulmcau  26523  ulmcn  26527  ulmdvlem1  26528  radcnvlem1  26541  radcnvle  26548  psercn  26554  pserdvlem2  26556  pserdv  26557  abelth  26569  tanregt0  26669  dvlog2lem  26782  efopn  26788  logtayllem  26789  logccv  26793  cxplt3  26830  cxpmul2zd  26846  cxpltd  26849  cxpled  26850  cxplt3d  26865  cxple3d  26866  dvsqrt  26872  cxpcn3  26878  cxpaddle  26882  cxpeq  26887  angcan  26932  angvald  26934  ang180lem2  26940  ang180  26944  isosctrlem3  26950  dquartlem1  26981  atantayl2  27068  leibpi  27072  log2tlbnd  27075  birthdaylem3  27083  xrlimcnp  27098  efrlim  27099  o1cxp  27104  jensenlem2  27117  jensen  27118  fsumharmonic  27141  lgamucov  27167  lgamcvg2  27184  wilthlem1  27197  basellem3  27212  basellem6  27215  basellem8  27217  ppisval  27233  chtwordi  27285  ppiwordi  27291  mumullem2  27309  mpodvdsmulf1o  27323  dvdsmulf1o  27325  fsumvma  27342  fsumvma2  27343  chpchtsum  27348  chpub  27349  logfacubnd  27350  dchrmulcl  27378  dchrinv  27390  dchrptlem1  27393  dchrptlem2  27394  sumdchr2  27399  dchr2sum  27402  bposlem7  27419  lgslem1  27426  lgslem3  27428  lgsdirprm  27460  lgsqrlem2  27476  lgseisenlem1  27504  lgseisenlem2  27505  lgseisenlem4  27507  lgseisen  27508  lgsquadlem1  27509  lgsquad2lem1  27513  lgsquad3  27516  m1lgs  27517  2sqlem7  27553  2sq2  27562  2sqmod  27565  chebbnd1lem2  27599  chebbnd1lem3  27600  rplogsumlem1  27613  rpvmasumlem  27616  dchrvmasumlem1  27624  dchrvmasum2lem  27625  dchrvmasumlema  27629  dchrisum0flblem2  27638  dchrisum0fno1  27640  dchrisum0re  27642  logdivsum  27662  pntrsumbnd2  27696  pntpbnd1a  27714  pntpbnd1  27715  pntibndlem2  27720  pntlemr  27731  pntlemj  27732  pntlemf  27734  pnt2  27742  padicabv  27759  ostth2lem2  27763  lesrecd  27958  ltsrecd  27960  madebday  28058  addsproplem6  28132  negsproplem6  28191  mulsproplem13  28286  mulsproplem14  28287  ltmulsd  28295  mulsgt0d  28303  f1otrg  29160  brbtwn2  29195  colinearalglem2  29197  axcgrtr  29205  axcgrid  29206  axsegconlem7  29213  axsegcon  29217  ax5seglem3  29221  ax5seglem6  29224  ax5seg  29228  axpaschlem  29230  axlowdimlem17  29248  axcontlem2  29255  axcontlem4  29257  axcontlem7  29260  axcontlem8  29261  ecgrtg  29273  usgredg2v  29517  vtxdgoddnumeven  29843  2trlond  30228  eupthp1  30507  nmobndi  31067  ubthlem2  31163  ubthlem3  31164  minvecolem2  31167  shuni  31592  pjhthlem1  31683  chscllem2  31930  pjcompi  31964  mayete3i  32020  unoplin  32212  hmoplin  32234  nmophmi  32323  mdslmd4i  32625  isoun  32987  submuladdd  33025  receqid  33029  xrge0addcld  33047  xrofsup  33052  eliccelico  33062  elicoelioo  33063  difioo  33067  rexdiv  33185  mgcmnt1d  33257  mgcmnt2d  33258  xrge0addgt0  33277  cycpmcl  33376  cycpm2tr  33379  cyc3evpm  33410  cycpmconjslem2  33415  fldgensdrg  33577  qusker  33611  eqgvscpbl  33612  ringlsmss1  33650  ringlsmss2  33651  intlidl  33671  lidlunitel  33674  elrspunidl  33679  idlinsubrg  33682  mxidlmaxv  33695  mxidlprm  33697  ssmxidllem  33700  opprmxidlabs  33713  qsdrnglem2  33722  dflring3  33731  dflring4  33732  selvply1rhmlem4  33857  mplvrpmmhm  33880  mplvrpmrhm  33881  esplyind  33909  resssra  33921  ply1degltdimlem  33956  lindsunlem  33958  sdrgfldext  33984  fldsdrgfldext  33995  finexttrb  33999  fldgenfldext  34002  fldextrspunlem1  34009  algextdeglem4  34054  algextdeglem8  34058  constrextdg2lem  34082  mdetpmtr2  34158  mdetpmtr12  34159  madjusmdetlem1  34161  madjusmdetlem4  34164  rhmpreimacn  34219  unitdivcld  34235  xrge0mulc1cn  34275  qqhnm  34324  esumcst  34397  esumfsup  34404  esumpmono  34413  esumcvg  34420  difelsiga  34467  sigapisys  34489  sigapildsys  34496  ldgenpisyslem1  34497  1stmbfm  34594  2ndmbfm  34595  dya2icoseg  34611  sibfinima  34673  probmeasb  34764  orvcgteel  34802  orvclteel  34807  ballotlemsima  34850  ballotlemfrceq  34863  ccatmulgnn0dir  34876  fct2relem  34928  ftc2re  34929  chtvalz  34960  r1filimi  35438  subfacp1lem2a  35570  subfaclim  35578  erdsze2lem2  35594  cvmliftlem2  35676  cvmliftlem10  35684  cvmliftlem13  35686  cvmliftiota  35691  cvmlift2lem9  35701  cvmlift2lem11  35703  cvmlift2lem12  35704  cvmliftphtlem  35707  cvmlift3lem6  35714  cvmlift3lem7  35715  cvmlift3lem9  35717  snmlff  35719  mrsubfval  35898  wzel  36212  wsuclem  36213  brsegle  36498  opnregcld  36729  weiunfrlem  36863  fin2so  38145  poimirlem17  38175  poimirlem23  38181  opnmbllem0  38194  mblfinlem3  38197  mblfinlem4  38198  itg2addnclem  38209  itg2addnc  38212  itg2gt0cn  38213  ftc1cnnclem  38229  ftc1cnnc  38230  areacirclem5  38250  indexdom  38272  sstotbnd2  38312  isbnd3  38322  isbnd3b  38323  cntotbnd  38334  ismtyima  38341  heibor1lem  38347  heiborlem8  38356  rrncmslem  38370  reheibor  38377  lkrlsp  39765  lshpkrlem5  39777  ldualssvscl  39821  ldualssvsubcl  39822  llnmlplnN  40202  llncvrlpln  40221  pmapjat1  40516  pclfinN  40563  lautlt  40754  lauteq  40758  lautco  40760  ltrn11  40789  ltrnle  40792  ltrneq2  40811  cdlemednuN  40963  cdleme20k  40982  cdleme20l2  40984  cdleme20l  40985  cdleme20m  40986  cdleme21c  40990  cdleme22e  41007  cdleme22eALTN  41008  cdlemefrs32fva  41063  cdlemg4g  41279  cdlemg18b  41342  cdlemg18c  41343  cdlemj3  41486  dia2dimlem5  41731  dvhopN  41779  cdlemm10N  41781  dihjatcclem4  42084  dochexmidlem2  42124  lclkrlem2o  42184  lcfrlem5  42209  lcfrlem6  42210  lcdlssvscl  42269  mapdpglem6  42341  mapdpglem9  42343  mapdpglem12  42346  mapdpglem14  42348  mapdindp0  42382  hdmaprnlem7N  42518  hdmaprnlem8N  42519  hdmaprnlem3eN  42521  hgmapvvlem3  42588  dvun  43009  addinvcom  43082  mzpsubst  43370  eldioph2lem1  43382  eldioph2lem2  43383  eldioph2b  43385  diophin  43394  irrapxlem2  43441  irrapxlem4  43443  irrapxlem5  43444  pellexlem1  43447  pellexlem2  43448  pellexlem6  43452  elpell1qr2  43490  pell1qrgaplem  43491  pell1qrgap  43492  pellqrex  43497  pellfundex  43504  pellfund14  43516  rmspecsqrtnq  43524  rmxyadd  43539  congsub  43588  mzpcong  43590  congrep  43591  acongtr  43596  acongrep  43598  jm2.19lem1  43607  jm2.22  43613  jm2.23  43614  jm2.26lem3  43619  jm2.26  43620  jm2.27a  43623  fnwe2lem2  43669  aomclem6  43677  hbtlem2  43742  hbtlem4  43744  hbtlem5  43746  dgraa0p  43767  rngunsnply  43787  proot1hash  43813  nnoeomeqom  43930  cantnf2  43943  omabs2  43950  naddcnff  43980  naddcnffo  43982  naddcnfcom  43984  naddcnfid1  43985  expgrowth  44936  fpmd  45869  abslt2sqd  45967  ioondisj2  46100  ioondisj1  46101  eliocre  46116  ioossioobi  46124  iooiinicc  46149  iooiinioc  46163  lptioo2  46238  limcresiooub  46247  limsupequzlem  46327  xlimmnfvlem2  46438  xlimpnfvlem2  46442  cncfuni  46491  cncfiooicclem1  46498  cxpcncf2  46504  dvcnre  46521  dvresntr  46523  dvresioo  46526  dvbdfbdioolem1  46533  dvnmptdivc  46543  dvnxpaek  46547  itgsinexplem1  46559  itgcoscmulx  46574  itgiccshift  46585  itgperiod  46586  ovolsplit  46593  stoweidlem11  46616  stoweidlem26  46631  stoweidlem34  46639  stoweidlem36  46641  stoweidlem38  46643  stirlinglem5  46683  dirkercncflem2  46709  dirkercncflem4  46711  fourierdlem20  46732  fourierdlem58  46769  fourierdlem72  46783  fourierdlem73  46784  fourierdlem74  46785  fourierdlem75  46786  fourierdlem76  46787  fourierdlem79  46790  fourierdlem80  46791  fourierdlem87  46798  fourierdlem94  46805  fourierdlem103  46814  fourierdlem104  46815  fourierdlem107  46818  fourierdlem113  46824  sqwvfoura  46833  sqwvfourb  46834  fourierswlem  46835  fouriersw  46836  etransclem46  46885  etransclem47  46886  rrndistlt  46895  rrnprjdstle  46906  ioorrnopnxrlem  46911  sge0ssre  47002  sge0seq  47051  hsphoidmvle2  47190  hsphoidmvle  47191  hoidmv1lelem1  47196  hoidmv1lelem2  47197  hoidmv1lelem3  47198  hoidmvlelem1  47200  hoidifhspdmvle  47225  hoiqssbllem2  47228  ovolval5lem2  47258  iinhoiicc  47279  iunhoiioo  47281  vonioolem2  47286  vonicclem2  47289  issmflem  47332  submodlt  47981  iccpartdisj  48074  m1expevenALTV  48300  fpprel2  48394  tgoldbach  48470  opstrgric  48579  gpg3kgrtriex  48742  nn0eo  49192  fdivpm  49207  refdivpm  49208  elbigolo1  49221  logbpw2m1  49231  fllog2  49232  dignn0flhalflem1  49279  dignn0flhalflem2  49280  itsclinecirc0in  49439  2itscplem2  49443  itscnhlinecirc02plem1  49446  iccdisj2  49559