Theorem syl22anc 838

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 836	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  4810  fr2nr  5596  soltmin  6087  f1oprg  6814  f1prex  7224  fveqf1o  7242  weniso  7294  fr3nr  7711  suppofssd  8139  smogt  8293  smocdmdom  8294  oacomf1o  8486  en2prd  8976  difsnen  8979  enfixsn  9006  domss2  9056  ssenen  9071  marypha1lem  9324  fisupcl  9361  ordtypelem3  9413  ordtypelem8  9418  oieu  9432  oismo  9433  wofib  9438  wemaplem2  9440  wemapso  9444  wemapso2lem  9445  unxpwdom2  9481  infdifsn  9554  oemapvali  9581  cantnflem1c  9584  cantnflem1  9586  cantnf  9590  cnfcom3  9601  r1ordg  9678  dif1card  9908  infxpenlem  9911  dfac8clem  9930  infxp  10112  infmap2  10115  cflim2  10161  coftr  10171  fin2i2  10216  enfin2i  10219  fin23lem26  10223  fin23lem27  10226  fin23lem40  10249  isf32lem2  10252  isf32lem3  10253  isf32lem4  10254  isf32lem7  10257  isf32lem9  10259  fin1a2lem13  10310  fin12  10311  alephexp1  10477  gchdomtri  10527  fpwwe2lem11  10539  fpwwe2lem12  10540  gchpwdom  10568  gchhar  10577  adderpqlem  10852  mulerpqlem  10853  addassnq  10856  mulassnq  10857  distrnq  10859  mulidnq  10861  recmulnq  10862  ltexnq  10873  distrlem1pr  10923  distrlem4pr  10924  prlem936  10945  reclem3pr  10947  mulcmpblnr  10969  mulgt0d  11275  mul4d  11332  add4d  11349  add42d  11350  subcan  11423  addsub4d  11526  subadd4d  11527  sub4d  11528  2addsubd  11529  addsubeq4d  11530  muladdd  11582  mulsubd  11583  addgegt0d  11697  addgtge0d  11698  addge0d  11700  mulge0d  11701  le2subd  11744  ltleaddd  11745  leltaddd  11746  lt2subd  11748  divdivdiv  11829  divcan5  11830  divne0d  11920  recdivd  11921  recdiv2d  11922  divcan6d  11923  ddcand  11924  rec11d  11925  divmuldivd  11945  divmul13d  11946  divmul24d  11947  divadddivd  11948  divsubdivd  11949  divmuleqd  11950  divdivdivd  11951  mulge0b  11999  recreclt  12028  divgt0d  12064  mulgt1d  12065  lemulge11d  12066  lemulge12d  12067  ltmul12ad  12070  lemul12ad  12071  lemul12bd  12072  supmul1  12098  nndivtr  12179  qreccl  12869  ledivdivd  12961  lediv12ad  12995  lt2mul2divd  13005  xlt2add  13161  supxrun  13217  supxrre  13228  infxrre  13238  elicore  13300  iccss2  13319  iccssico2  13322  icossico2d  13323  lincmb01cmp  13397  iccf1o  13398  fzrev2i  13491  2tnp1ge0ge0  13735  m1modnnsub1  13826  modaddmodup  13843  modaddmodlo  13844  modsubdir  13849  fzennn  13877  sermono  13943  mulexpz  14011  expaddz  14015  sqdiv  14030  expsubd  14066  ltexp2a  14075  expmordi  14076  leexp2a  14081  expmulnbnd  14144  digit1  14146  lt2sqd  14165  le2sqd  14166  sq11d  14167  bcm1k  14224  bcp1n  14225  bcp1nk  14226  hashf1lem1  14364  cshw1  14731  2swrd2eqwrdeq  14862  ofccat  14878  absrele  15217  sqreulem  15269  sqrtmuld  15334  sqrtsq2d  15335  sqrtled  15336  sqrtltd  15337  sqr11d  15338  abs3lemd  15373  rlimuni  15459  climuni  15461  lo1resb  15473  o1resb  15475  2clim  15481  addcn2  15503  mulcn2  15505  o1of2  15522  o1rlimmul  15528  lo1add  15536  lo1mul  15537  isercolllem1  15574  caucvgrlem  15582  iseraltlem2  15592  iseraltlem3  15593  mptfzshft  15687  fsumrev  15688  fsum0diag2  15692  binomlem  15738  climcndslem1  15758  climcndslem2  15759  harmonic  15768  mertenslem1  15793  fprodser  15858  fprodrev  15886  efcllem  15986  moddvds  16176  dvds1  16232  dvdsext  16234  evennn2n  16264  bitsinv1  16355  sadaddlem  16379  sadasslem  16383  sadeq  16385  mulgcd  16461  dvdssqlem  16479  lcmftp  16549  rpmulgcd2  16569  coprmproddvdslem  16575  isprm5  16620  isprm6  16627  crth  16691  eulerthlem2  16695  prmdiveq  16699  pythagtriplem11  16739  pythagtriplem13  16741  pcgcd1  16791  pcprmpw2  16796  pcaddlem  16802  fldivp1  16811  4sqlem12  16870  4sqlem14  16872  4sqlem15  16873  4sqlem16  16874  vdwapun  16888  mreexexlem4d  17555  acsfn1  17569  acsfn2  17571  sscpwex  17724  rescabs  17742  yonedainv  18189  chnub  18530  subm0  18725  pmtrfb  19379  psgnunilem1  19407  odmodnn0  19454  odeq  19464  dfod2  19478  sylow1lem1  19512  lsmsubg  19568  lsmmod  19589  lsmdisj2  19596  ghmplusg  19760  odadd  19764  gexexlem  19766  lt6abl  19809  cyggex2  19811  dprdfinv  19935  dmdprdsplitlem  19953  dpjidcl  19974  ablfacrp  19982  ablfacrp2  19983  ablfac1c  19987  ablfac1eu  19989  omndadd2d  20044  omndadd2rd  20045  omndmul2  20047  acsfn1p  20716  lcomfsupp  20837  lssvancl1  20880  lssvnegcl  20891  lspprvacl  20934  ellspsni  20936  lspsn  20937  lmhmplusg  20980  lmhmima  20983  lmhmpreima  20984  reslmhm  20988  lbsind2  21017  lsmcl  21019  lsmelval2  21021  lsppreli  21026  lspprabs  21031  pj1lmhm  21036  lssvs0or  21049  lspabs3  21060  lspfixed  21067  lspexch  21068  lsmcv  21080  lspsolv  21082  drngnidl  21182  rhmpreimaidl  21216  rngqiprngimfo  21240  rngqiprngfulem4  21253  gzrngunit  21372  zringlpirlem3  21403  prmirredlem  21411  znf1o  21490  znunithash  21503  freshmansdream  21513  ofldchr  21515  frlmsubgval  21704  frlmvplusgvalc  21706  frlmvscaval  21707  frlmphllem  21719  frlmphl  21720  frlmssuvc1  21733  frlmsslsp  21735  frlmup1  21737  frlmup2  21738  lindfind2  21757  lindfrn  21760  f1lindf  21761  islindf4  21777  mplbas2  21978  evlslem3  22016  evlslem1  22018  coe1addfv  22180  lply1binom  22226  evl1addd  22257  evl1subd  22258  evl1muld  22259  mamudi  22319  mamudir  22320  1marepvmarrepid  22491  mdetrlin  22518  smadiadetglem1  22587  smadiadetg  22589  cramerimplem1  22599  mat2pmatscmxcl  22656  m2pmfzgsumcl  22664  pmatcollpw  22697  pmatcollpwfi  22698  pmatcollpw3fi1lem1  22702  cpmidpmatlem2  22787  cpmadugsumlemF  22792  chcoeffeqlem  22801  ntrin  22977  topssnei  23040  restbas  23074  restntr  23098  cnntri  23187  fiuncmp  23320  nllyrest  23402  nllyidm  23405  hausllycmp  23410  cldllycmp  23411  hauspwdom  23417  txcld  23519  txcn  23542  txlly  23552  txnlly  23553  txhaus  23563  txlm  23564  txkgen  23568  xkococnlem  23575  cnmpt2res  23593  xkoinjcn  23603  basqtop  23627  qtopeu  23632  trfbas2  23759  neifil  23796  hausflim  23897  alexsubALTlem2  23964  cnextfval  23978  cnextfvval  23981  cnextf  23982  cnextfres  23985  clssubg  24025  utop2nei  24166  utop3cls  24167  utopreg  24168  psmetlecl  24231  xmetlecl  24262  prdsxmetlem  24284  bldisj  24314  imasf1obl  24404  prdsbl  24407  stdbdmet  24432  stdbdmopn  24434  met2ndci  24438  metcnp  24457  metustto  24469  metustexhalf  24472  cfilucfil  24475  metucn  24487  lssnlm  24617  nmotri  24655  nmoid  24658  tgioo  24712  blcvx  24714  xrsmopn  24729  reperflem  24735  reconnlem2  24744  opnreen  24748  metdsge  24766  metdsre  24770  metdscnlem  24772  metnrmlem1a  24775  metnrmlem1  24776  metnrmlem3  24778  cncfmet  24830  cnmpopc  24850  icopnfcnv  24868  icopnfhmeo  24869  cnllycmp  24883  evth  24886  lebnumii  24893  nmoleub2lem3  25043  iscfil2  25194  cfil3i  25197  iscfil3  25201  cfilfcls  25202  iscau3  25206  iscmet3lem2  25220  caubl  25236  lmcau  25241  cssbn  25303  rrxcph  25320  minveclem2  25354  pjthlem1  25365  pjthlem2  25366  ivthicc  25387  ovollecl  25412  ovolunlem1a  25425  ovolunnul  25429  ovoliunlem1  25431  ismbl2  25456  nulmbl2  25465  unmbl  25466  volun  25474  voliunlem2  25480  ioombl1lem2  25488  uniioombllem2a  25511  uniioombllem3  25514  uniioombllem4  25515  dyaddisjlem  25524  dyadmaxlem  25526  opnmbllem  25530  volsup2  25534  volcn  25535  ismbfd  25568  mbfi1fseqlem1  25644  mbfi1fseqlem5  25648  itg2lecl  25667  itg2monolem2  25680  itg2gt0  25689  itgspliticc  25766  ellimc3  25808  limcres  25815  dvfval  25826  dvres3  25842  dvres3a  25843  dvmptresicc  25845  dvnff  25853  dvnadd  25859  dvn2bss  25860  dvnres  25861  dvcmul  25875  dvcmulf  25876  dvmptres3  25888  dvmptres2  25894  dvmptntr  25903  dvexp3  25910  dvferm1lem  25916  dvlip  25926  dvlipcn  25927  dvlip2  25928  c1liplem1  25929  dvgt0lem1  25935  dvgt0lem2  25936  dvne0  25944  lhop1lem  25946  lhop2  25948  lhop  25949  dvcnvrelem1  25950  dvcnvrelem2  25951  dvcvx  25953  dvfsumle  25954  dvfsumleOLD  25955  dvfsumabs  25957  dvfsumlem2  25961  dvfsumlem2OLD  25962  ftc1lem6  25976  ftc1  25977  ftc2ditglem  25980  itgsubstlem  25983  itgpowd  25985  tdeglem4  25993  mdegaddle  26007  mdegmullem  26011  ply1rem  26099  fta1glem2  26102  fta1blem  26104  ig1peu  26108  ig1pdvds  26113  dgrmulc  26205  dgrcolem1  26207  plydivlem4  26232  plydiveu  26234  fta1lem  26243  vieta1lem1  26246  vieta1lem2  26247  plyexmo  26249  taylfvallem1  26292  taylfval  26294  tayl0  26297  taylplem1  26298  taylply2  26303  taylply2OLD  26304  taylply  26305  dvtaylp  26306  dvntaylp  26307  dvntaylp0  26308  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  ulmcaulem  26331  ulmcau  26332  ulmcn  26336  ulmdvlem1  26337  radcnvlem1  26350  radcnvle  26357  psercn  26364  pserdvlem2  26366  pserdv  26367  abelth  26379  tanregt0  26476  dvlog2lem  26589  efopn  26595  logtayllem  26596  logccv  26600  cxplt3  26637  cxpmul2zd  26653  cxpltd  26656  cxpled  26657  cxplt3d  26672  cxple3d  26673  dvsqrt  26679  cxpcn3  26686  cxpaddle  26690  cxpeq  26695  angcan  26740  angvald  26742  ang180lem2  26748  ang180  26752  isosctrlem3  26758  dquartlem1  26789  atantayl2  26876  leibpi  26880  log2tlbnd  26883  birthdaylem3  26891  xrlimcnp  26906  efrlim  26907  efrlimOLD  26908  o1cxp  26913  jensenlem2  26926  jensen  26927  fsumharmonic  26950  lgamucov  26976  lgamcvg2  26993  wilthlem1  27006  basellem3  27021  basellem6  27024  basellem8  27026  ppisval  27042  chtwordi  27094  ppiwordi  27100  mumullem2  27118  mpodvdsmulf1o  27132  dvdsmulf1o  27134  fsumvma  27152  fsumvma2  27153  chpchtsum  27158  chpub  27159  logfacubnd  27160  dchrmulcl  27188  dchrinv  27200  dchrptlem1  27203  dchrptlem2  27204  sumdchr2  27209  dchr2sum  27212  bposlem7  27229  lgslem1  27236  lgslem3  27238  lgsdirprm  27270  lgsqrlem2  27286  lgseisenlem1  27314  lgseisenlem2  27315  lgseisenlem4  27317  lgseisen  27318  lgsquadlem1  27319  lgsquad2lem1  27323  lgsquad3  27326  m1lgs  27327  2sqlem7  27363  2sq2  27372  2sqmod  27375  chebbnd1lem2  27409  chebbnd1lem3  27410  rplogsumlem1  27423  rpvmasumlem  27426  dchrvmasumlem1  27434  dchrvmasum2lem  27435  dchrvmasumlema  27439  dchrisum0flblem2  27448  dchrisum0fno1  27450  dchrisum0re  27452  logdivsum  27472  pntrsumbnd2  27506  pntpbnd1a  27524  pntpbnd1  27525  pntibndlem2  27530  pntlemr  27541  pntlemj  27542  pntlemf  27544  pnt2  27552  padicabv  27569  ostth2lem2  27573  slerecd  27762  sltrecd  27764  madebday  27846  addsproplem6  27918  negsproplem6  27976  mulsproplem13  28068  mulsproplem14  28069  sltmuld  28077  mulsgt0d  28085  f1otrg  28850  brbtwn2  28885  colinearalglem2  28887  axcgrtr  28895  axcgrid  28896  axsegconlem7  28903  axsegcon  28907  ax5seglem3  28911  ax5seglem6  28914  ax5seg  28918  axpaschlem  28920  axlowdimlem17  28938  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  axcontlem8  28951  ecgrtg  28963  usgredg2v  29207  vtxdgoddnumeven  29534  2trlond  29919  eupthp1  30198  nmobndi  30757  ubthlem2  30853  ubthlem3  30854  minvecolem2  30857  shuni  31282  pjhthlem1  31373  chscllem2  31620  pjcompi  31654  mayete3i  31710  unoplin  31902  hmoplin  31924  nmophmi  32013  mdslmd4i  32315  isoun  32687  submuladdd  32727  receqid  32732  xrge0addcld  32749  xrofsup  32754  eliccelico  32764  elicoelioo  32765  difioo  32769  hashpss  32796  sgnmul  32823  rexdiv  32913  mgcmnt1d  32985  mgcmnt2d  32986  xrge0addgt0  33005  cycpmcl  33092  cycpm2tr  33095  cyc3evpm  33126  cycpmconjslem2  33131  fldgensdrg  33287  qusker  33321  eqgvscpbl  33322  ringlsmss1  33368  ringlsmss2  33369  lidlmcld  33391  intlidl  33392  lidlunitel  33395  elrspunidl  33400  idlinsubrg  33403  isprmidlc  33419  rhmpreimaprmidl  33423  qsidomlem1  33424  ssdifidllem  33428  mxidlmaxv  33440  mxidlprm  33442  ssmxidllem  33445  opprmxidlabs  33459  qsdrnglem2  33468  mplvrpmmhm  33594  mplvrpmrhm  33595  esplyind  33613  resssra  33620  ply1degltdimlem  33656  lindsunlem  33658  sdrgfldext  33684  fldsdrgfldext  33695  finexttrb  33699  fldgenfldext  33702  fldextrspunlem1  33709  algextdeglem4  33754  algextdeglem8  33758  constrextdg2lem  33782  mdetpmtr2  33858  mdetpmtr12  33859  madjusmdetlem1  33861  madjusmdetlem4  33864  rhmpreimacn  33919  unitdivcld  33935  xrge0mulc1cn  33975  qqhnm  34024  esumcst  34097  esumfsup  34104  esumpmono  34113  esumcvg  34120  difelsiga  34167  sigapisys  34189  sigapildsys  34196  ldgenpisyslem1  34197  1stmbfm  34294  2ndmbfm  34295  dya2icoseg  34311  sibfinima  34373  probmeasb  34464  orvcgteel  34502  orvclteel  34507  ballotlemsima  34550  ballotlemfrceq  34563  ccatmulgnn0dir  34576  fct2relem  34631  ftc2re  34632  chtvalz  34663  r1filimi  35135  subfacp1lem2a  35245  subfaclim  35253  erdsze2lem2  35269  cvmliftlem2  35351  cvmliftlem10  35359  cvmliftlem13  35361  cvmliftiota  35366  cvmlift2lem9  35376  cvmlift2lem11  35378  cvmlift2lem12  35379  cvmliftphtlem  35382  cvmlift3lem6  35389  cvmlift3lem7  35390  cvmlift3lem9  35392  snmlff  35394  mrsubfval  35573  wzel  35887  wsuclem  35888  brsegle  36173  opnregcld  36395  weiunfrlem  36529  fin2so  37667  poimirlem17  37697  poimirlem23  37703  opnmbllem0  37716  mblfinlem3  37719  mblfinlem4  37720  itg2addnclem  37731  itg2addnc  37734  itg2gt0cn  37735  ftc1cnnclem  37751  ftc1cnnc  37752  areacirclem5  37772  indexdom  37794  sstotbnd2  37834  isbnd3  37844  isbnd3b  37845  cntotbnd  37856  ismtyima  37863  heibor1lem  37869  heiborlem8  37878  rrncmslem  37892  reheibor  37899  lkrlsp  39221  lshpkrlem5  39233  ldualssvscl  39277  ldualssvsubcl  39278  llnmlplnN  39658  llncvrlpln  39677  pmapjat1  39972  pclfinN  40019  lautlt  40210  lauteq  40214  lautco  40216  ltrn11  40245  ltrnle  40248  ltrneq2  40267  cdlemednuN  40419  cdleme20k  40438  cdleme20l2  40440  cdleme20l  40441  cdleme20m  40442  cdleme21c  40446  cdleme22e  40463  cdleme22eALTN  40464  cdlemefrs32fva  40519  cdlemg4g  40735  cdlemg18b  40798  cdlemg18c  40799  cdlemj3  40942  dia2dimlem5  41187  dvhopN  41235  cdlemm10N  41237  dihjatcclem4  41540  dochexmidlem2  41580  lclkrlem2o  41640  lcfrlem5  41665  lcfrlem6  41666  lcdlssvscl  41725  mapdpglem6  41797  mapdpglem9  41799  mapdpglem12  41802  mapdpglem14  41804  mapdindp0  41838  hdmaprnlem7N  41974  hdmaprnlem8N  41975  hdmaprnlem3eN  41977  hgmapvvlem3  42044  dvun  42477  addinvcom  42550  evlsaddval  42686  evlsmulval  42687  evladdval  42693  evlmulval  42694  mzpsubst  42865  eldioph2lem1  42877  eldioph2lem2  42878  eldioph2b  42880  diophin  42889  irrapxlem2  42940  irrapxlem4  42942  irrapxlem5  42943  pellexlem1  42946  pellexlem2  42947  pellexlem6  42951  elpell1qr2  42989  pell1qrgaplem  42990  pell1qrgap  42991  pellqrex  42996  pellfundex  43003  pellfund14  43015  rmspecsqrtnq  43023  rmxyadd  43038  congsub  43087  mzpcong  43089  congrep  43090  acongtr  43095  acongrep  43097  jm2.19lem1  43106  jm2.22  43112  jm2.23  43113  jm2.26lem3  43118  jm2.26  43119  jm2.27a  43122  fnwe2lem2  43168  aomclem6  43176  hbtlem2  43241  hbtlem4  43243  hbtlem5  43245  dgraa0p  43266  rngunsnply  43286  proot1hash  43312  nnoeomeqom  43429  cantnf2  43442  omabs2  43449  naddcnff  43479  naddcnffo  43481  naddcnfcom  43483  naddcnfid1  43484  expgrowth  44452  fpmd  45384  abslt2sqd  45483  ioondisj2  45617  ioondisj1  45618  eliocre  45633  ioossioobi  45641  iooiinicc  45666  iooiinioc  45680  lptioo2  45755  limcresiooub  45764  limsupequzlem  45844  xlimmnfvlem2  45955  xlimpnfvlem2  45959  cncfuni  46008  cncfiooicclem1  46015  cxpcncf2  46021  dvcnre  46038  dvresntr  46040  dvresioo  46043  dvbdfbdioolem1  46050  dvnmptdivc  46060  dvnxpaek  46064  itgsinexplem1  46076  itgcoscmulx  46091  itgiccshift  46102  itgperiod  46103  ovolsplit  46110  stoweidlem11  46133  stoweidlem26  46148  stoweidlem34  46156  stoweidlem36  46158  stoweidlem38  46160  stirlinglem5  46200  dirkercncflem2  46226  dirkercncflem4  46228  fourierdlem20  46249  fourierdlem58  46286  fourierdlem72  46300  fourierdlem73  46301  fourierdlem74  46302  fourierdlem75  46303  fourierdlem76  46304  fourierdlem79  46307  fourierdlem80  46308  fourierdlem87  46315  fourierdlem94  46322  fourierdlem103  46331  fourierdlem104  46332  fourierdlem107  46335  fourierdlem113  46341  sqwvfoura  46350  sqwvfourb  46351  fourierswlem  46352  fouriersw  46353  etransclem46  46402  etransclem47  46403  rrndistlt  46412  rrnprjdstle  46423  ioorrnopnxrlem  46428  sge0ssre  46519  sge0seq  46568  hsphoidmvle2  46707  hsphoidmvle  46708  hoidmv1lelem1  46713  hoidmv1lelem2  46714  hoidmv1lelem3  46715  hoidmvlelem1  46717  hoidifhspdmvle  46742  hoiqssbllem2  46745  ovolval5lem2  46775  iinhoiicc  46796  iunhoiioo  46798  vonioolem2  46803  vonicclem2  46806  issmflem  46849  submodlt  47474  iccpartdisj  47561  m1expevenALTV  47771  fpprel2  47865  tgoldbach  47941  opstrgric  48050  gpg3kgrtriex  48213  nn0eo  48653  fdivpm  48668  refdivpm  48669  elbigolo1  48682  logbpw2m1  48692  fllog2  48693  dignn0flhalflem1  48740  dignn0flhalflem2  48741  itsclinecirc0in  48900  2itscplem2  48904  itscnhlinecirc02plem1  48907  iccdisj2  49021