Theorem syl22anc 839

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  preqsnd  4803  fr2nr  5602  soltmin  6094  f1oprg  6821  f1prex  7233  fveqf1o  7251  weniso  7303  fr3nr  7720  suppofssd  8147  smogt  8301  smocdmdom  8302  oacomf1o  8494  en2prd  8988  difsnen  8991  enfixsn  9018  domss2  9068  ssenen  9083  marypha1lem  9340  fisupcl  9377  ordtypelem3  9429  ordtypelem8  9434  oieu  9448  oismo  9449  wofib  9454  wemaplem2  9456  wemapso  9460  wemapso2lem  9461  unxpwdom2  9497  infdifsn  9572  oemapvali  9599  cantnflem1c  9602  cantnflem1  9604  cantnf  9608  cnfcom3  9619  r1ordg  9696  dif1card  9926  infxpenlem  9929  dfac8clem  9948  infxp  10130  infmap2  10133  cflim2  10179  coftr  10189  fin2i2  10234  enfin2i  10237  fin23lem26  10241  fin23lem27  10244  fin23lem40  10267  isf32lem2  10270  isf32lem3  10271  isf32lem4  10272  isf32lem7  10275  isf32lem9  10277  fin1a2lem13  10328  fin12  10329  alephexp1  10496  gchdomtri  10546  fpwwe2lem11  10558  fpwwe2lem12  10559  gchpwdom  10587  gchhar  10596  adderpqlem  10871  mulerpqlem  10872  addassnq  10875  mulassnq  10876  distrnq  10878  mulidnq  10880  recmulnq  10881  ltexnq  10892  distrlem1pr  10942  distrlem4pr  10943  prlem936  10964  reclem3pr  10966  mulcmpblnr  10988  mulgt0d  11295  mul4d  11352  add4d  11369  add42d  11370  subcan  11443  addsub4d  11546  subadd4d  11547  sub4d  11548  2addsubd  11549  addsubeq4d  11550  muladdd  11602  mulsubd  11603  addgegt0d  11717  addgtge0d  11718  addge0d  11720  mulge0d  11721  le2subd  11764  ltleaddd  11765  leltaddd  11766  lt2subd  11768  divdivdiv  11850  divcan5  11851  divne0d  11941  recdivd  11942  recdiv2d  11943  divcan6d  11944  ddcand  11945  rec11d  11946  divmuldivd  11966  divmul13d  11967  divmul24d  11968  divadddivd  11969  divsubdivd  11970  divmuleqd  11971  divdivdivd  11972  mulge0b  12020  recreclt  12049  divgt0d  12085  mulgt1d  12086  lemulge11d  12087  lemulge12d  12088  ltmul12ad  12091  lemul12ad  12092  lemul12bd  12093  supmul1  12119  nndivtr  12218  qreccl  12913  ledivdivd  13005  lediv12ad  13039  lt2mul2divd  13049  xlt2add  13206  supxrun  13262  supxrre  13273  infxrre  13283  elicore  13345  iccss2  13364  iccssico2  13367  icossico2d  13368  lincmb01cmp  13442  iccf1o  13443  nnge2recico01  13454  fzrev2i  13537  2tnp1ge0ge0  13782  m1modnnsub1  13873  modaddmodup  13890  modaddmodlo  13891  modsubdir  13896  fzennn  13924  sermono  13990  mulexpz  14058  expaddz  14062  sqdiv  14077  expsubd  14113  ltexp2a  14122  expmordi  14123  leexp2a  14128  expmulnbnd  14191  digit1  14193  lt2sqd  14212  le2sqd  14213  sq11d  14214  bcm1k  14271  bcp1n  14272  bcp1nk  14273  hashf1lem1  14411  cshw1  14778  2swrd2eqwrdeq  14909  ofccat  14925  absrele  15264  sqreulem  15316  sqrtmuld  15381  sqrtsq2d  15382  sqrtled  15383  sqrtltd  15384  sqr11d  15385  abs3lemd  15420  rlimuni  15506  climuni  15508  lo1resb  15520  o1resb  15522  2clim  15528  addcn2  15550  mulcn2  15552  o1of2  15569  o1rlimmul  15575  lo1add  15583  lo1mul  15584  isercolllem1  15621  caucvgrlem  15629  iseraltlem2  15639  iseraltlem3  15640  mptfzshft  15734  fsumrev  15735  fsum0diag2  15739  binomlem  15788  climcndslem1  15808  climcndslem2  15809  harmonic  15818  mertenslem1  15843  fprodser  15908  fprodrev  15936  efcllem  16036  moddvds  16226  dvds1  16282  dvdsext  16284  evennn2n  16314  bitsinv1  16405  sadaddlem  16429  sadasslem  16433  sadeq  16435  mulgcd  16511  dvdssqlem  16529  lcmftp  16599  rpmulgcd2  16619  coprmproddvdslem  16625  isprm5  16671  isprm6  16678  crth  16742  eulerthlem2  16746  prmdiveq  16750  pythagtriplem11  16790  pythagtriplem13  16792  pcgcd1  16842  pcprmpw2  16847  pcaddlem  16853  fldivp1  16862  4sqlem12  16921  4sqlem14  16923  4sqlem15  16924  4sqlem16  16925  vdwapun  16939  mreexexlem4d  17607  acsfn1  17621  acsfn2  17623  sscpwex  17776  rescabs  17794  yonedainv  18241  chnub  18582  subm0  18777  pmtrfb  19434  psgnunilem1  19462  odmodnn0  19509  odeq  19519  dfod2  19533  sylow1lem1  19567  lsmsubg  19623  lsmmod  19644  lsmdisj2  19651  ghmplusg  19815  odadd  19819  gexexlem  19821  lt6abl  19864  cyggex2  19866  dprdfinv  19990  dmdprdsplitlem  20008  dpjidcl  20029  ablfacrp  20037  ablfacrp2  20038  ablfac1c  20042  ablfac1eu  20044  omndadd2d  20099  omndadd2rd  20100  omndmul2  20102  acsfn1p  20770  lcomfsupp  20891  lssvancl1  20934  lssvnegcl  20945  lspprvacl  20988  ellspsni  20990  lspsn  20991  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  21426  zringlpirlem3  21457  prmirredlem  21465  znf1o  21544  znunithash  21557  freshmansdream  21567  ofldchr  21569  frlmsubgval  21758  frlmvplusgvalc  21760  frlmvscaval  21761  frlmphllem  21773  frlmphl  21774  frlmssuvc1  21787  frlmsslsp  21789  frlmup1  21791  frlmup2  21792  lindfind2  21811  lindfrn  21814  f1lindf  21815  islindf4  21831  mplbas2  22033  evlslem3  22071  evlslem1  22073  evladdval  22094  evlmulval  22095  coe1addfv  22243  lply1binom  22288  evl1addd  22319  evl1subd  22320  evl1muld  22321  mamudi  22381  mamudir  22382  1marepvmarrepid  22553  mdetrlin  22580  smadiadetglem1  22649  smadiadetg  22651  cramerimplem1  22661  mat2pmatscmxcl  22718  m2pmfzgsumcl  22726  pmatcollpw  22759  pmatcollpwfi  22760  pmatcollpw3fi1lem1  22764  cpmidpmatlem2  22849  cpmadugsumlemF  22854  chcoeffeqlem  22863  ntrin  23039  topssnei  23102  restbas  23136  restntr  23160  cnntri  23249  fiuncmp  23382  nllyrest  23464  nllyidm  23467  hausllycmp  23472  cldllycmp  23473  hauspwdom  23479  txcld  23581  txcn  23604  txlly  23614  txnlly  23615  txhaus  23625  txlm  23626  txkgen  23630  xkococnlem  23637  cnmpt2res  23655  xkoinjcn  23665  basqtop  23689  qtopeu  23694  trfbas2  23821  neifil  23858  hausflim  23959  alexsubALTlem2  24026  cnextfval  24040  cnextfvval  24043  cnextf  24044  cnextfres  24047  clssubg  24087  utop2nei  24228  utop3cls  24229  utopreg  24230  psmetlecl  24293  xmetlecl  24324  prdsxmetlem  24346  bldisj  24376  imasf1obl  24466  prdsbl  24469  stdbdmet  24494  stdbdmopn  24496  met2ndci  24500  metcnp  24519  metustto  24531  metustexhalf  24534  cfilucfil  24537  metucn  24549  lssnlm  24679  nmotri  24717  nmoid  24720  tgioo  24774  blcvx  24776  xrsmopn  24791  reperflem  24797  reconnlem2  24806  opnreen  24810  metdsge  24828  metdsre  24832  metdscnlem  24834  metnrmlem1a  24837  metnrmlem1  24838  metnrmlem3  24840  cncfmet  24889  cnmpopc  24908  icopnfcnv  24922  icopnfhmeo  24923  cnllycmp  24936  evth  24939  lebnumii  24946  nmoleub2lem3  25095  iscfil2  25246  cfil3i  25249  iscfil3  25253  cfilfcls  25254  iscau3  25258  iscmet3lem2  25272  caubl  25288  lmcau  25293  cssbn  25355  rrxcph  25372  minveclem2  25406  pjthlem1  25417  pjthlem2  25418  ivthicc  25438  ovollecl  25463  ovolunlem1a  25476  ovolunnul  25480  ovoliunlem1  25482  ismbl2  25507  nulmbl2  25516  unmbl  25517  volun  25525  voliunlem2  25531  ioombl1lem2  25539  uniioombllem2a  25562  uniioombllem3  25565  uniioombllem4  25566  dyaddisjlem  25575  dyadmaxlem  25577  opnmbllem  25581  volsup2  25585  volcn  25586  ismbfd  25619  mbfi1fseqlem1  25695  mbfi1fseqlem5  25699  itg2lecl  25718  itg2monolem2  25731  itg2gt0  25740  itgspliticc  25817  ellimc3  25859  limcres  25866  dvfval  25877  dvres3  25893  dvres3a  25894  dvmptresicc  25896  dvnff  25903  dvnadd  25909  dvn2bss  25910  dvnres  25911  dvcmul  25924  dvcmulf  25925  dvmptres3  25936  dvmptres2  25942  dvmptntr  25951  dvexp3  25958  dvferm1lem  25964  dvlip  25973  dvlipcn  25974  dvlip2  25975  c1liplem1  25976  dvgt0lem1  25982  dvgt0lem2  25983  dvne0  25991  lhop1lem  25993  lhop2  25995  lhop  25996  dvcnvrelem1  25997  dvcnvrelem2  25998  dvcvx  26000  dvfsumle  26001  dvfsumabs  26003  dvfsumlem2  26007  ftc1lem6  26021  ftc1  26022  ftc2ditglem  26025  itgsubstlem  26028  itgpowd  26030  tdeglem4  26038  mdegaddle  26052  mdegmullem  26056  ply1rem  26144  fta1glem2  26147  fta1blem  26149  ig1peu  26153  ig1pdvds  26158  dgrmulc  26249  dgrcolem1  26251  plydivlem4  26276  plydiveu  26278  fta1lem  26287  vieta1lem1  26290  vieta1lem2  26291  plyexmo  26293  taylfvallem1  26336  taylfval  26338  tayl0  26341  taylplem1  26342  taylply2  26347  taylply2OLD  26348  taylply  26349  dvtaylp  26350  dvntaylp  26351  dvntaylp0  26352  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulmcaulem  26375  ulmcau  26376  ulmcn  26380  ulmdvlem1  26381  radcnvlem1  26394  radcnvle  26401  psercn  26407  pserdvlem2  26409  pserdv  26410  abelth  26422  tanregt0  26519  dvlog2lem  26632  efopn  26638  logtayllem  26639  logccv  26643  cxplt3  26680  cxpmul2zd  26696  cxpltd  26699  cxpled  26700  cxplt3d  26715  cxple3d  26716  dvsqrt  26722  cxpcn3  26728  cxpaddle  26732  cxpeq  26737  angcan  26782  angvald  26784  ang180lem2  26790  ang180  26794  isosctrlem3  26800  dquartlem1  26831  atantayl2  26918  leibpi  26922  log2tlbnd  26925  birthdaylem3  26933  xrlimcnp  26948  efrlim  26949  efrlimOLD  26950  o1cxp  26955  jensenlem2  26968  jensen  26969  fsumharmonic  26992  lgamucov  27018  lgamcvg2  27035  wilthlem1  27048  basellem3  27063  basellem6  27066  basellem8  27068  ppisval  27084  chtwordi  27136  ppiwordi  27142  mumullem2  27160  mpodvdsmulf1o  27174  dvdsmulf1o  27176  fsumvma  27193  fsumvma2  27194  chpchtsum  27199  chpub  27200  logfacubnd  27201  dchrmulcl  27229  dchrinv  27241  dchrptlem1  27244  dchrptlem2  27245  sumdchr2  27250  dchr2sum  27253  bposlem7  27270  lgslem1  27277  lgslem3  27279  lgsdirprm  27311  lgsqrlem2  27327  lgseisenlem1  27355  lgseisenlem2  27356  lgseisenlem4  27358  lgseisen  27359  lgsquadlem1  27360  lgsquad2lem1  27364  lgsquad3  27367  m1lgs  27368  2sqlem7  27404  2sq2  27413  2sqmod  27416  chebbnd1lem2  27450  chebbnd1lem3  27451  rplogsumlem1  27464  rpvmasumlem  27467  dchrvmasumlem1  27475  dchrvmasum2lem  27476  dchrvmasumlema  27480  dchrisum0flblem2  27489  dchrisum0fno1  27491  dchrisum0re  27493  logdivsum  27513  pntrsumbnd2  27547  pntpbnd1a  27565  pntpbnd1  27566  pntibndlem2  27571  pntlemr  27582  pntlemj  27583  pntlemf  27585  pnt2  27593  padicabv  27610  ostth2lem2  27614  lesrecd  27809  ltsrecd  27811  madebday  27909  addsproplem6  27983  negsproplem6  28042  mulsproplem13  28137  mulsproplem14  28138  ltmulsd  28146  mulsgt0d  28154  f1otrg  28956  brbtwn2  28991  colinearalglem2  28993  axcgrtr  29001  axcgrid  29002  axsegconlem7  29009  axsegcon  29013  ax5seglem3  29017  ax5seglem6  29020  ax5seg  29024  axpaschlem  29026  axlowdimlem17  29044  axcontlem2  29051  axcontlem4  29053  axcontlem7  29056  axcontlem8  29057  ecgrtg  29069  usgredg2v  29313  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  32793  submuladdd  32831  receqid  32835  xrge0addcld  32853  xrofsup  32858  eliccelico  32868  elicoelioo  32869  difioo  32873  hashpss  32900  sgnmul  32926  rexdiv  33003  mgcmnt1d  33075  mgcmnt2d  33076  xrge0addgt0  33095  cycpmcl  33195  cycpm2tr  33198  cyc3evpm  33229  cycpmconjslem2  33234  fldgensdrg  33393  qusker  33427  eqgvscpbl  33428  ringlsmss1  33474  ringlsmss2  33475  lidlmcld  33497  intlidl  33498  lidlunitel  33501  elrspunidl  33506  idlinsubrg  33509  isprmidlc  33525  rhmpreimaprmidl  33529  qsidomlem1  33530  ssdifidllem  33534  mxidlmaxv  33546  mxidlprm  33548  ssmxidllem  33551  opprmxidlabs  33565  qsdrnglem2  33574  mplvrpmmhm  33708  mplvrpmrhm  33709  esplyind  33737  resssra  33749  ply1degltdimlem  33785  lindsunlem  33787  sdrgfldext  33813  fldsdrgfldext  33824  finexttrb  33828  fldgenfldext  33831  fldextrspunlem1  33838  algextdeglem4  33883  algextdeglem8  33887  constrextdg2lem  33911  mdetpmtr2  33987  mdetpmtr12  33988  madjusmdetlem1  33990  madjusmdetlem4  33993  rhmpreimacn  34048  unitdivcld  34064  xrge0mulc1cn  34104  qqhnm  34153  esumcst  34226  esumfsup  34233  esumpmono  34242  esumcvg  34249  difelsiga  34296  sigapisys  34318  sigapildsys  34325  ldgenpisyslem1  34326  1stmbfm  34423  2ndmbfm  34424  dya2icoseg  34440  sibfinima  34502  probmeasb  34593  orvcgteel  34631  orvclteel  34636  ballotlemsima  34679  ballotlemfrceq  34692  ccatmulgnn0dir  34705  fct2relem  34760  ftc2re  34761  chtvalz  34792  r1filimi  35265  subfacp1lem2a  35381  subfaclim  35389  erdsze2lem2  35405  cvmliftlem2  35487  cvmliftlem10  35495  cvmliftlem13  35497  cvmliftiota  35502  cvmlift2lem9  35512  cvmlift2lem11  35514  cvmlift2lem12  35515  cvmliftphtlem  35518  cvmlift3lem6  35525  cvmlift3lem7  35526  cvmlift3lem9  35528  snmlff  35530  mrsubfval  35709  wzel  36023  wsuclem  36024  brsegle  36309  opnregcld  36531  weiunfrlem  36665  fin2so  37945  poimirlem17  37975  poimirlem23  37981  opnmbllem0  37994  mblfinlem3  37997  mblfinlem4  37998  itg2addnclem  38009  itg2addnc  38012  itg2gt0cn  38013  ftc1cnnclem  38029  ftc1cnnc  38030  areacirclem5  38050  indexdom  38072  sstotbnd2  38112  isbnd3  38122  isbnd3b  38123  cntotbnd  38134  ismtyima  38141  heibor1lem  38147  heiborlem8  38156  rrncmslem  38170  reheibor  38177  lkrlsp  39565  lshpkrlem5  39577  ldualssvscl  39621  ldualssvsubcl  39622  llnmlplnN  40002  llncvrlpln  40021  pmapjat1  40316  pclfinN  40363  lautlt  40554  lauteq  40558  lautco  40560  ltrn11  40589  ltrnle  40592  ltrneq2  40611  cdlemednuN  40763  cdleme20k  40782  cdleme20l2  40784  cdleme20l  40785  cdleme20m  40786  cdleme21c  40790  cdleme22e  40807  cdleme22eALTN  40808  cdlemefrs32fva  40863  cdlemg4g  41079  cdlemg18b  41142  cdlemg18c  41143  cdlemj3  41286  dia2dimlem5  41531  dvhopN  41579  cdlemm10N  41581  dihjatcclem4  41884  dochexmidlem2  41924  lclkrlem2o  41984  lcfrlem5  42009  lcfrlem6  42010  lcdlssvscl  42069  mapdpglem6  42141  mapdpglem9  42143  mapdpglem12  42146  mapdpglem14  42148  mapdindp0  42182  hdmaprnlem7N  42318  hdmaprnlem8N  42319  hdmaprnlem3eN  42321  hgmapvvlem3  42388  dvun  42808  addinvcom  42881  evlsaddval  43021  evlsmulval  43022  mzpsubst  43197  eldioph2lem1  43209  eldioph2lem2  43210  eldioph2b  43212  diophin  43221  irrapxlem2  43272  irrapxlem4  43274  irrapxlem5  43275  pellexlem1  43278  pellexlem2  43279  pellexlem6  43283  elpell1qr2  43321  pell1qrgaplem  43322  pell1qrgap  43323  pellqrex  43328  pellfundex  43335  pellfund14  43347  rmspecsqrtnq  43355  rmxyadd  43370  congsub  43419  mzpcong  43421  congrep  43422  acongtr  43427  acongrep  43429  jm2.19lem1  43438  jm2.22  43444  jm2.23  43445  jm2.26lem3  43450  jm2.26  43451  jm2.27a  43454  fnwe2lem2  43500  aomclem6  43508  hbtlem2  43573  hbtlem4  43575  hbtlem5  43577  dgraa0p  43598  rngunsnply  43618  proot1hash  43644  nnoeomeqom  43761  cantnf2  43774  omabs2  43781  naddcnff  43811  naddcnffo  43813  naddcnfcom  43815  naddcnfid1  43816  expgrowth  44783  fpmd  45713  abslt2sqd  45811  ioondisj2  45944  ioondisj1  45945  eliocre  45960  ioossioobi  45968  iooiinicc  45993  iooiinioc  46007  lptioo2  46082  limcresiooub  46091  limsupequzlem  46171  xlimmnfvlem2  46282  xlimpnfvlem2  46286  cncfuni  46335  cncfiooicclem1  46342  cxpcncf2  46348  dvcnre  46365  dvresntr  46367  dvresioo  46370  dvbdfbdioolem1  46377  dvnmptdivc  46387  dvnxpaek  46391  itgsinexplem1  46403  itgcoscmulx  46418  itgiccshift  46429  itgperiod  46430  ovolsplit  46437  stoweidlem11  46460  stoweidlem26  46475  stoweidlem34  46483  stoweidlem36  46485  stoweidlem38  46487  stirlinglem5  46527  dirkercncflem2  46553  dirkercncflem4  46555  fourierdlem20  46576  fourierdlem58  46613  fourierdlem72  46627  fourierdlem73  46628  fourierdlem74  46629  fourierdlem75  46630  fourierdlem76  46631  fourierdlem79  46634  fourierdlem80  46635  fourierdlem87  46642  fourierdlem94  46649  fourierdlem103  46658  fourierdlem104  46659  fourierdlem107  46662  fourierdlem113  46668  sqwvfoura  46677  sqwvfourb  46678  fourierswlem  46679  fouriersw  46680  etransclem46  46729  etransclem47  46730  rrndistlt  46739  rrnprjdstle  46750  ioorrnopnxrlem  46755  sge0ssre  46846  sge0seq  46895  hsphoidmvle2  47034  hsphoidmvle  47035  hoidmv1lelem1  47040  hoidmv1lelem2  47041  hoidmv1lelem3  47042  hoidmvlelem1  47044  hoidifhspdmvle  47069  hoiqssbllem2  47072  ovolval5lem2  47102  iinhoiicc  47123  iunhoiioo  47125  vonioolem2  47130  vonicclem2  47133  issmflem  47176  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