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  4824  fr2nr  5638  soltmin  6136  f1oprg  6867  f1prex  7282  fveqf1o  7300  weniso  7352  fr3nr  7767  suppofssd  8195  smogt  8350  smocdmdom  8351  oacomf1o  8546  en2prd  9040  difsnen  9043  enfixsn  9070  domss2  9120  ssenen  9135  marypha1lem  9389  fisupcl  9426  ordtypelem3  9478  ordtypelem8  9483  oieu  9497  oismo  9498  wofib  9503  wemaplem2  9505  wemapso  9509  wemapso2lem  9510  unxpwdom2  9546  infdifsn  9622  oemapvali  9649  cantnflem1c  9652  cantnflem1  9654  cantnf  9658  cnfcom3  9669  r1ordg  9746  dif1card  9990  infxpenlem  9993  dfac8clem  10012  infxp  10193  infmap2  10196  cflim2  10242  coftr  10252  fin2i2  10297  enfin2i  10300  fin23lem26  10304  fin23lem27  10307  fin23lem40  10330  isf32lem2  10333  isf32lem3  10334  isf32lem4  10335  isf32lem7  10338  isf32lem9  10340  fin1a2lem13  10391  fin12  10392  alephexp1  10559  gchdomtri  10609  fpwwe2lem11  10621  fpwwe2lem12  10622  gchpwdom  10650  gchhar  10659  adderpqlem  10934  mulerpqlem  10935  addassnq  10938  mulassnq  10939  distrnq  10941  mulidnq  10943  recmulnq  10944  ltexnq  10955  distrlem1pr  11005  distrlem4pr  11006  prlem936  11027  reclem3pr  11029  mulcmpblnr  11051  mulgt0d  11360  mul4d  11417  add4d  11434  add42d  11435  subcan  11508  addsub4d  11611  subadd4d  11612  sub4d  11613  2addsubd  11614  addsubeq4d  11615  muladdd  11667  mulsubd  11668  addgegt0d  11782  addgtge0d  11783  addge0d  11785  mulge0d  11786  le2subd  11829  ltleaddd  11830  leltaddd  11831  lt2subd  11833  divdivdiv  11911  divcan5  11912  divne0d  12002  recdivd  12003  recdiv2d  12004  divcan6d  12005  ddcand  12006  rec11d  12007  divmuldivd  12027  divmul13d  12028  divmul24d  12029  divadddivd  12030  divsubdivd  12031  divmuleqd  12032  divdivdivd  12033  mulge0b  12080  recreclt  12109  divgt0d  12145  mulgt1d  12146  lemulge11d  12147  lemulge12d  12148  ltmul12ad  12151  lemul12ad  12152  lemul12bd  12153  supmul1  12179  nndivtr  12278  qreccl  12988  ledivdivd  13080  lediv12ad  13114  lt2mul2divd  13124  xlt2add  13281  supxrun  13337  supxrre  13348  infxrre  13358  elicore  13420  iccss2  13439  iccssico2  13442  icossico2d  13443  lincmb01cmp  13517  iccf1o  13518  nnge2recico01  13529  fzrev2i  13613  2tnp1ge0ge0  13858  m1modnnsub1  13949  modaddmodup  13966  modaddmodlo  13967  modsubdir  13972  fzennn  14000  sermono  14066  mulexpz  14134  expaddz  14138  sqdiv  14153  expsubd  14189  ltexp2a  14198  expmordi  14199  leexp2a  14204  expmulnbnd  14267  digit1  14269  lt2sqd  14288  le2sqd  14289  sq11d  14290  bcm1k  14347  bcp1n  14348  bcp1nk  14349  hashpss  14442  hashf1lem1  14488  cshw1  14855  2swrd2eqwrdeq  14986  ofccat  15002  sgnmul  15140  absrele  15355  sqreulem  15407  sqrtmuld  15472  sqrtsq2d  15473  sqrtled  15474  sqrtltd  15475  sqr11d  15476  abs3lemd  15511  rlimuni  15597  climuni  15599  lo1resb  15611  o1resb  15613  2clim  15619  addcn2  15641  mulcn2  15643  o1of2  15660  o1rlimmul  15666  lo1add  15674  lo1mul  15675  isercolllem1  15712  caucvgrlem  15720  iseraltlem2  15730  iseraltlem3  15731  mptfzshft  15825  fsumrev  15826  fsum0diag2  15830  binomlem  15879  climcndslem1  15899  climcndslem2  15900  harmonic  15909  mertenslem1  15934  fprodser  15999  fprodrev  16027  efcllem  16126  moddvds  16316  dvds1  16372  dvdsext  16374  evennn2n  16404  bitsinv1  16495  sadaddlem  16519  sadasslem  16523  sadeq  16525  mulgcd  16601  dvdssqlem  16619  lcmftp  16689  rpmulgcd2  16709  coprmproddvdslem  16715  isprm5  16761  isprm6  16768  crth  16832  eulerthlem2  16836  prmdiveq  16840  pythagtriplem11  16880  pythagtriplem13  16882  pcgcd1  16932  pcprmpw2  16937  pcaddlem  16943  fldivp1  16952  4sqlem12  17011  4sqlem14  17013  4sqlem15  17014  4sqlem16  17015  vdwapun  17029  mreexexlem4d  17698  acsfn1  17712  acsfn2  17714  sscpwex  17867  rescabs  17885  yonedainv  18332  chnub  18673  subm0  18869  pmtrfb  19530  psgnunilem1  19558  odmodnn0  19605  odeq  19615  dfod2  19629  sylow1lem1  19663  lsmsubg  19719  lsmmod  19740  lsmdisj2  19747  ghmplusg  19911  odadd  19915  gexexlem  19917  lt6abl  19960  cyggex2  19962  dprdfinv  20086  dmdprdsplitlem  20104  dpjidcl  20125  ablfacrp  20133  ablfacrp2  20134  ablfac1c  20138  ablfac1eu  20140  omndadd2d  20195  omndadd2rd  20196  omndmul2  20198  acsfn1p  20902  lcomfsupp  21023  lssvancl1  21066  lssvnegcl  21077  lspprvacl  21120  ellspsni  21122  lspsn  21123  lmhmplusg  21165  lmhmima  21168  lmhmpreima  21169  reslmhm  21173  lbsind2  21202  lsmcl  21204  lsmelval2  21206  lsppreli  21211  lspprabs  21216  pj1lmhm  21221  lssvs0or  21234  lspabs3  21245  lspfixed  21252  lspexch  21253  lsmcv  21265  lspsolv  21267  lidlmcld  21352  drngnidl  21377  rhmpreimaidl  21416  rngqiprngimfo  21441  rngqiprngfulem4  21454  isprmidlc  21472  rhmpreimaprmidl  21479  qsidomlem1  21480  ssdifidllem  21484  gzrngunit  21583  zringlpirlem3  21614  prmirredlem  21622  znf1o  21701  znunithash  21714  freshmansdream  21724  ofldchr  21726  frlmsubgval  21915  frlmvplusgvalc  21917  frlmvscaval  21918  frlmphllem  21930  frlmphl  21931  frlmssuvc1  21944  frlmsslsp  21946  frlmup1  21948  frlmup2  21949  lindfind2  21968  lindfrn  21971  f1lindf  21972  islindf4  21988  mplbas2  22193  evlslem3  22231  evlslem1  22233  evladdval  22254  evlmulval  22255  evlsaddval  22280  evlsmulval  22281  coe1addfv  22426  lply1binom  22470  evl1addd  22501  evl1subd  22502  evl1muld  22503  mamudi  22560  mamudir  22561  1marepvmarrepid  22732  mdetrlin  22759  smadiadetglem1  22828  smadiadetg  22830  cramerimplem1  22840  mat2pmatscmxcl  22897  m2pmfzgsumcl  22905  pmatcollpw  22938  pmatcollpwfi  22939  pmatcollpw3fi1lem1  22943  cpmidpmatlem2  23028  cpmadugsumlemF  23033  chcoeffeqlem  23042  ntrin  23218  topssnei  23281  restbas  23315  restntr  23339  cnntri  23428  fiuncmp  23561  nllyrest  23643  nllyidm  23646  hausllycmp  23651  cldllycmp  23652  hauspwdom  23658  txcld  23760  txcn  23783  txlly  23793  txnlly  23794  txhaus  23804  txlm  23805  txkgen  23809  xkococnlem  23816  cnmpt2res  23834  xkoinjcn  23844  basqtop  23868  qtopeu  23873  trfbas2  24000  neifil  24037  hausflim  24138  alexsubALTlem2  24205  cnextfval  24219  cnextfvval  24222  cnextf  24223  cnextfres  24226  clssubg  24266  utop2nei  24407  utop3cls  24408  utopreg  24409  psmetlecl  24472  xmetlecl  24503  prdsxmetlem  24525  bldisj  24555  imasf1obl  24645  prdsbl  24648  stdbdmet  24673  stdbdmopn  24675  met2ndci  24679  metcnp  24698  metustto  24710  metustexhalf  24713  cfilucfil  24716  metucn  24728  lssnlm  24858  nmotri  24896  nmoid  24899  tgioo  24953  blcvx  24955  xrsmopn  24970  reperflem  24976  reconnlem2  24985  opnreen  24989  metdsge  25007  metdsre  25011  metdscnlem  25013  metnrmlem1a  25016  metnrmlem1  25017  metnrmlem3  25019  cncfmet  25068  cnmpopc  25087  icopnfcnv  25101  icopnfhmeo  25102  cnllycmp  25115  evth  25118  lebnumii  25125  nmoleub2lem3  25274  iscfil2  25425  cfil3i  25428  iscfil3  25432  cfilfcls  25433  iscau3  25437  iscmet3lem2  25451  caubl  25467  lmcau  25472  cssbn  25534  rrxcph  25551  minveclem2  25585  pjthlem1  25596  pjthlem2  25597  ivthicc  25617  ovollecl  25642  ovolunlem1a  25655  ovolunnul  25659  ovoliunlem1  25661  ismbl2  25686  nulmbl2  25695  unmbl  25696  volun  25704  voliunlem2  25710  ioombl1lem2  25718  uniioombllem2a  25741  uniioombllem3  25744  uniioombllem4  25745  dyaddisjlem  25754  dyadmaxlem  25756  opnmbllem  25760  volsup2  25764  volcn  25765  ismbfd  25798  mbfi1fseqlem1  25874  mbfi1fseqlem5  25878  itg2lecl  25897  itg2monolem2  25910  itg2gt0  25919  itgspliticc  25996  ellimc3  26038  limcres  26045  dvfval  26056  dvres3  26072  dvres3a  26073  dvmptresicc  26075  dvnff  26082  dvnadd  26088  dvn2bss  26089  dvnres  26090  dvcmul  26103  dvcmulf  26104  dvmptres3  26115  dvmptres2  26121  dvmptntr  26130  dvexp3  26137  dvferm1lem  26143  dvlip  26152  dvlipcn  26153  dvlip2  26154  c1liplem1  26155  dvgt0lem1  26161  dvgt0lem2  26162  dvne0  26170  lhop1lem  26172  lhop2  26174  lhop  26175  dvcnvrelem1  26176  dvcnvrelem2  26177  dvcvx  26179  dvfsumle  26180  dvfsumabs  26182  dvfsumlem2  26186  ftc1lem6  26200  ftc1  26201  ftc2ditglem  26204  itgsubstlem  26207  itgpowd  26209  tdeglem4  26217  mdegaddle  26231  mdegmullem  26235  ply1rem  26323  fta1glem2  26326  fta1blem  26328  ig1peu  26332  ig1pdvds  26337  dgrmulc  26428  dgrcolem1  26430  plydivlem4  26457  plydiveu  26459  fta1lem  26468  vieta1lem1  26471  vieta1lem2  26472  plyexmo  26474  taylfvallem1  26520  taylfval  26522  tayl0  26525  taylplem1  26526  taylply2  26531  taylply  26532  dvtaylp  26533  dvntaylp  26534  dvntaylp0  26535  taylthlem1  26536  taylthlem2  26537  ulmcaulem  26557  ulmcau  26558  ulmcn  26562  ulmdvlem1  26563  radcnvlem1  26576  radcnvle  26583  psercn  26589  pserdvlem2  26591  pserdv  26592  abelth  26604  tanregt0  26704  dvlog2lem  26817  efopn  26823  logtayllem  26824  logccv  26828  cxplt3  26865  cxpmul2zd  26881  cxpltd  26884  cxpled  26885  cxplt3d  26900  cxple3d  26901  dvsqrt  26907  cxpcn3  26913  cxpaddle  26917  cxpeq  26922  angcan  26967  angvald  26969  ang180lem2  26975  ang180  26979  isosctrlem3  26985  dquartlem1  27016  atantayl2  27103  leibpi  27107  log2tlbnd  27110  birthdaylem3  27118  xrlimcnp  27133  efrlim  27134  o1cxp  27139  jensenlem2  27152  jensen  27153  fsumharmonic  27176  lgamucov  27202  lgamcvg2  27219  wilthlem1  27232  basellem3  27247  basellem6  27250  basellem8  27252  ppisval  27268  chtwordi  27320  ppiwordi  27326  mumullem2  27344  mpodvdsmulf1o  27358  dvdsmulf1o  27360  fsumvma  27377  fsumvma2  27378  chpchtsum  27383  chpub  27384  logfacubnd  27385  dchrmulcl  27413  dchrinv  27425  dchrptlem1  27428  dchrptlem2  27429  sumdchr2  27434  dchr2sum  27437  bposlem7  27454  lgslem1  27461  lgslem3  27463  lgsdirprm  27495  lgsqrlem2  27511  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem4  27542  lgseisen  27543  lgsquadlem1  27544  lgsquad2lem1  27548  lgsquad3  27551  m1lgs  27552  2sqlem7  27588  2sq2  27597  2sqmod  27600  chebbnd1lem2  27634  chebbnd1lem3  27635  rplogsumlem1  27648  rpvmasumlem  27651  dchrvmasumlem1  27659  dchrvmasum2lem  27660  dchrvmasumlema  27664  dchrisum0flblem2  27673  dchrisum0fno1  27675  dchrisum0re  27677  logdivsum  27697  pntrsumbnd2  27731  pntpbnd1a  27749  pntpbnd1  27750  pntibndlem2  27755  pntlemr  27766  pntlemj  27767  pntlemf  27769  pnt2  27777  padicabv  27794  ostth2lem2  27798  lesrecd  27993  ltsrecd  27995  madebday  28093  addsproplem6  28167  negsproplem6  28226  mulsproplem13  28321  mulsproplem14  28322  ltmulsd  28330  mulsgt0d  28338  f1otrg  29220  brbtwn2  29255  colinearalglem2  29257  axcgrtr  29265  axcgrid  29266  axsegconlem7  29273  axsegcon  29277  ax5seglem3  29281  ax5seglem6  29284  ax5seg  29288  axpaschlem  29290  axlowdimlem17  29308  axcontlem2  29315  axcontlem4  29317  axcontlem7  29320  axcontlem8  29321  ecgrtg  29333  usgredg2v  29577  vtxdgoddnumeven  29903  2trlond  30288  eupthp1  30567  nmobndi  31127  ubthlem2  31223  ubthlem3  31224  minvecolem2  31227  shuni  31652  pjhthlem1  31743  chscllem2  31990  pjcompi  32024  mayete3i  32080  unoplin  32272  hmoplin  32294  nmophmi  32383  mdslmd4i  32685  isoun  33047  submuladdd  33085  receqid  33089  xrge0addcld  33107  xrofsup  33112  eliccelico  33122  elicoelioo  33123  difioo  33127  rexdiv  33245  mgcmnt1d  33317  mgcmnt2d  33318  xrge0addgt0  33337  cycpmcl  33436  cycpm2tr  33439  cyc3evpm  33470  cycpmconjslem2  33475  fldgensdrg  33635  qusker  33669  eqgvscpbl  33670  ringlsmss1  33707  ringlsmss2  33708  intlidl  33728  lidlunitel  33731  elrspunidl  33736  idlinsubrg  33739  mxidlmaxv  33751  mxidlprm  33753  ssmxidllem  33756  opprmxidlabs  33769  qsdrnglem2  33778  dflring3  33787  dflring4  33788  selvply1rhmlem4  33913  mplvrpmmhm  33936  mplvrpmrhm  33937  esplyind  33965  resssra  33977  ply1degltdimlem  34012  lindsunlem  34014  sdrgfldext  34040  fldsdrgfldext  34051  finexttrb  34055  fldgenfldext  34058  fldextrspunlem1  34065  algextdeglem4  34110  algextdeglem8  34114  constrextdg2lem  34138  mdetpmtr2  34214  mdetpmtr12  34215  madjusmdetlem1  34217  madjusmdetlem4  34220  rhmpreimacn  34275  unitdivcld  34291  xrge0mulc1cn  34331  qqhnm  34380  esumcst  34453  esumfsup  34460  esumpmono  34469  esumcvg  34476  difelsiga  34523  sigapisys  34545  sigapildsys  34552  ldgenpisyslem1  34553  1stmbfm  34650  2ndmbfm  34651  dya2icoseg  34667  sibfinima  34729  probmeasb  34820  orvcgteel  34858  orvclteel  34863  ballotlemsima  34906  ballotlemfrceq  34919  ccatmulgnn0dir  34932  fct2relem  34984  ftc2re  34985  chtvalz  35016  r1filimi  35497  subfacp1lem2a  35672  subfaclim  35680  erdsze2lem2  35696  cvmliftlem2  35778  cvmliftlem10  35786  cvmliftlem13  35788  cvmliftiota  35793  cvmlift2lem9  35803  cvmlift2lem11  35805  cvmlift2lem12  35806  cvmliftphtlem  35809  cvmlift3lem6  35816  cvmlift3lem7  35817  cvmlift3lem9  35819  snmlff  35821  mrsubfval  36000  wzel  36314  wsuclem  36315  brsegle  36600  nmulel1  36692  opnregcld  36841  weiunfrlem  36975  fin2so  38258  poimirlem17  38288  poimirlem23  38294  opnmbllem0  38307  mblfinlem3  38310  mblfinlem4  38311  itg2addnclem  38322  itg2addnc  38325  itg2gt0cn  38326  ftc1cnnclem  38342  ftc1cnnc  38343  areacirclem5  38363  indexdom  38385  sstotbnd2  38425  isbnd3  38435  isbnd3b  38436  cntotbnd  38447  ismtyima  38454  heibor1lem  38460  heiborlem8  38469  rrncmslem  38483  reheibor  38490  lkrlsp  39876  lshpkrlem5  39888  ldualssvscl  39932  ldualssvsubcl  39933  llnmlplnN  40313  llncvrlpln  40332  pmapjat1  40627  pclfinN  40674  lautlt  40865  lauteq  40869  lautco  40871  ltrn11  40900  ltrnle  40903  ltrneq2  40922  cdlemednuN  41074  cdleme20k  41093  cdleme20l2  41095  cdleme20l  41096  cdleme20m  41097  cdleme21c  41101  cdleme22e  41118  cdleme22eALTN  41119  cdlemefrs32fva  41174  cdlemg4g  41390  cdlemg18b  41453  cdlemg18c  41454  cdlemj3  41597  dia2dimlem5  41842  dvhopN  41890  cdlemm10N  41892  dihjatcclem4  42195  dochexmidlem2  42235  lclkrlem2o  42295  lcfrlem5  42320  lcfrlem6  42321  lcdlssvscl  42380  mapdpglem6  42452  mapdpglem9  42454  mapdpglem12  42457  mapdpglem14  42459  mapdindp0  42493  hdmaprnlem7N  42629  hdmaprnlem8N  42630  hdmaprnlem3eN  42632  hgmapvvlem3  42699  dvun  43120  addinvcom  43193  mzpsubst  43479  eldioph2lem1  43491  eldioph2lem2  43492  eldioph2b  43494  diophin  43503  irrapxlem2  43550  irrapxlem4  43552  irrapxlem5  43553  pellexlem1  43556  pellexlem2  43557  pellexlem6  43561  elpell1qr2  43599  pell1qrgaplem  43600  pell1qrgap  43601  pellqrex  43606  pellfundex  43613  pellfund14  43625  rmspecsqrtnq  43633  rmxyadd  43648  congsub  43697  mzpcong  43699  congrep  43700  acongtr  43705  acongrep  43707  jm2.19lem1  43716  jm2.22  43722  jm2.23  43723  jm2.26lem3  43728  jm2.26  43729  jm2.27a  43732  fnwe2lem2  43778  aomclem6  43786  hbtlem2  43851  hbtlem4  43853  hbtlem5  43855  dgraa0p  43876  rngunsnply  43896  proot1hash  43922  nnoeomeqom  44039  cantnf2  44052  omabs2  44059  naddcnff  44089  naddcnffo  44091  naddcnfcom  44093  naddcnfid1  44094  expgrowth  45045  fpmd  45978  abslt2sqd  46076  ioondisj2  46209  ioondisj1  46210  eliocre  46225  ioossioobi  46233  iooiinicc  46258  iooiinioc  46272  lptioo2  46347  limcresiooub  46356  limsupequzlem  46436  xlimmnfvlem2  46547  xlimpnfvlem2  46551  cncfuni  46600  cncfiooicclem1  46607  cxpcncf2  46613  dvcnre  46630  dvresntr  46632  dvresioo  46635  dvbdfbdioolem1  46642  dvnmptdivc  46652  dvnxpaek  46656  itgsinexplem1  46668  itgcoscmulx  46683  itgiccshift  46694  itgperiod  46695  ovolsplit  46702  stoweidlem11  46725  stoweidlem26  46740  stoweidlem34  46748  stoweidlem36  46750  stoweidlem38  46752  stirlinglem5  46792  dirkercncflem2  46818  dirkercncflem4  46820  fourierdlem20  46841  fourierdlem58  46878  fourierdlem72  46892  fourierdlem73  46893  fourierdlem74  46894  fourierdlem75  46895  fourierdlem76  46896  fourierdlem79  46899  fourierdlem80  46900  fourierdlem87  46907  fourierdlem94  46914  fourierdlem103  46923  fourierdlem104  46924  fourierdlem107  46927  fourierdlem113  46933  sqwvfoura  46942  sqwvfourb  46943  fourierswlem  46944  fouriersw  46945  etransclem46  46994  etransclem47  46995  rrndistlt  47004  rrnprjdstle  47015  ioorrnopnxrlem  47020  sge0ssre  47111  sge0seq  47160  hsphoidmvle2  47299  hsphoidmvle  47300  hoidmv1lelem1  47305  hoidmv1lelem2  47306  hoidmv1lelem3  47307  hoidmvlelem1  47309  hoidifhspdmvle  47334  hoiqssbllem2  47337  ovolval5lem2  47367  iinhoiicc  47388  iunhoiioo  47390  vonioolem2  47395  vonicclem2  47398  issmflem  47441  submodlt  48093  iccpartdisj  48186  m1expevenALTV  48412  fpprel2  48506  tgoldbach  48582  opstrgric  48691  gpg3kgrtriex  48854  nn0eo  49308  fdivpm  49323  refdivpm  49324  elbigolo1  49337  logbpw2m1  49347  fllog2  49348  dignn0flhalflem1  49395  dignn0flhalflem2  49396  itsclinecirc0in  49555  2itscplem2  49559  itscnhlinecirc02plem1  49562  iccdisj2  49675