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  4859  fr2nr  5662  soltmin  6156  f1oprg  6893  f1prex  7304  fveqf1o  7322  weniso  7374  fr3nr  7792  suppofssd  8228  smogt  8407  smocdmdom  8408  oacomf1o  8603  en2prd  9088  enpr2dOLD  9090  difsnen  9093  undomOLD  9100  enfixsn  9121  domss2  9176  ssenen  9191  marypha1lem  9473  fisupcl  9509  ordtypelem3  9560  ordtypelem8  9565  oieu  9579  oismo  9580  wofib  9585  wemaplem2  9587  wemapso  9591  wemapso2lem  9592  unxpwdom2  9628  infdifsn  9697  oemapvali  9724  cantnflem1c  9727  cantnflem1  9729  cantnf  9733  cnfcom3  9744  r1ordg  9818  dif1card  10050  infxpenlem  10053  dfac8clem  10072  infxp  10254  infmap2  10257  cflim2  10303  coftr  10313  fin2i2  10358  enfin2i  10361  fin23lem26  10365  fin23lem27  10368  fin23lem40  10391  isf32lem2  10394  isf32lem3  10395  isf32lem4  10396  isf32lem7  10399  isf32lem9  10401  fin1a2lem13  10452  fin12  10453  alephexp1  10619  gchdomtri  10669  fpwwe2lem11  10681  fpwwe2lem12  10682  gchpwdom  10710  gchhar  10719  adderpqlem  10994  mulerpqlem  10995  addassnq  10998  mulassnq  10999  distrnq  11001  mulidnq  11003  recmulnq  11004  ltexnq  11015  distrlem1pr  11065  distrlem4pr  11066  prlem936  11087  reclem3pr  11089  mulcmpblnr  11111  mulgt0d  11416  mul4d  11473  add4d  11490  add42d  11491  subcan  11564  addsub4d  11667  subadd4d  11668  sub4d  11669  2addsubd  11670  addsubeq4d  11671  muladdd  11721  mulsubd  11722  addgegt0d  11836  addgtge0d  11837  addge0d  11839  mulge0d  11840  le2addd  11882  le2subd  11883  ltleaddd  11884  leltaddd  11885  lt2subd  11887  divdivdiv  11968  divcan5  11969  divne0d  12059  recdivd  12060  recdiv2d  12061  divcan6d  12062  ddcand  12063  rec11d  12064  divmuldivd  12084  divmul13d  12085  divmul24d  12086  divadddivd  12087  divsubdivd  12088  divmuleqd  12089  divdivdivd  12090  subrecd  12098  mulge0b  12138  recreclt  12167  divgt0d  12203  mulgt1d  12204  lemulge11d  12205  lemulge12d  12206  ltmul12ad  12209  lemul12ad  12210  lemul12bd  12211  supmul1  12237  nndivtr  12313  qreccl  13011  ledivdivd  13102  lediv12ad  13136  lt2mul2divd  13146  xlt2add  13302  supxrun  13358  supxrre  13369  infxrre  13378  elicore  13439  iccss2  13458  iccssico2  13461  lincmb01cmp  13535  iccf1o  13536  fzrev2i  13629  2tnp1ge0ge0  13869  m1modnnsub1  13958  modaddmodup  13975  modaddmodlo  13976  modsubdir  13981  fzennn  14009  sermono  14075  mulexpz  14143  expaddz  14147  sqdiv  14161  expsubd  14197  ltexp2a  14206  expmordi  14207  leexp2a  14212  expmulnbnd  14274  digit1  14276  lt2sqd  14295  le2sqd  14296  sq11d  14297  bcm1k  14354  bcp1n  14355  bcp1nk  14356  hashf1lem1  14494  cshw1  14860  2swrd2eqwrdeq  14992  ofccat  15008  absrele  15347  sqreulem  15398  sqrtmuld  15463  sqrtsq2d  15464  sqrtled  15465  sqrtltd  15466  sqr11d  15467  abs3lemd  15500  rlimuni  15586  climuni  15588  lo1resb  15600  o1resb  15602  2clim  15608  addcn2  15630  mulcn2  15632  o1of2  15649  o1rlimmul  15655  lo1add  15663  lo1mul  15664  isercolllem1  15701  caucvgrlem  15709  iseraltlem2  15719  iseraltlem3  15720  mptfzshft  15814  fsumrev  15815  fsum0diag2  15819  binomlem  15865  climcndslem1  15885  climcndslem2  15886  harmonic  15895  mertenslem1  15920  fprodser  15985  fprodrev  16013  efcllem  16113  moddvds  16301  dvds1  16356  dvdsext  16358  evennn2n  16388  bitsinv1  16479  sadaddlem  16503  sadasslem  16507  sadeq  16509  mulgcd  16585  dvdssqlem  16603  lcmftp  16673  rpmulgcd2  16693  coprmproddvdslem  16699  isprm5  16744  isprm6  16751  crth  16815  eulerthlem2  16819  prmdiveq  16823  pythagtriplem11  16863  pythagtriplem13  16865  pcgcd1  16915  pcprmpw2  16920  pcaddlem  16926  fldivp1  16935  4sqlem12  16994  4sqlem14  16996  4sqlem15  16997  4sqlem16  16998  vdwapun  17012  mreexexlem4d  17690  acsfn1  17704  acsfn2  17706  sscpwex  17859  rescabs  17877  rescabsOLD  17878  yonedainv  18326  subm0  18828  pmtrfb  19483  psgnunilem1  19511  odmodnn0  19558  odeq  19568  dfod2  19582  sylow1lem1  19616  lsmsubg  19672  lsmmod  19693  lsmdisj2  19700  ghmplusg  19864  odadd  19868  gexexlem  19870  lt6abl  19913  cyggex2  19915  dprdfinv  20039  dmdprdsplitlem  20057  dpjidcl  20078  ablfacrp  20086  ablfacrp2  20087  ablfac1c  20091  ablfac1eu  20093  acsfn1p  20800  lcomfsupp  20900  lssvancl1  20943  lssvnegcl  20954  lspprvacl  20997  ellspsni  20999  lspsn  21000  lmhmplusg  21043  lmhmima  21046  lmhmpreima  21047  reslmhm  21051  lbsind2  21080  lsmcl  21082  lsmelval2  21084  lsppreli  21089  lspprabs  21094  pj1lmhm  21099  lssvs0or  21112  lspabs3  21123  lspfixed  21130  lspexch  21131  lsmcv  21143  lspsolv  21145  drngnidl  21253  rhmpreimaidl  21287  rngqiprngimfo  21311  rngqiprngfulem4  21324  gzrngunit  21451  zringlpirlem3  21475  prmirredlem  21483  znf1o  21570  znunithash  21583  freshmansdream  21593  frlmsubgval  21785  frlmvplusgvalc  21787  frlmvscaval  21788  frlmphllem  21800  frlmphl  21801  frlmssuvc1  21814  frlmsslsp  21816  frlmup1  21818  frlmup2  21819  lindfind2  21838  lindfrn  21841  f1lindf  21842  islindf4  21858  mplbas2  22060  evlslem3  22104  evlslem1  22106  coe1addfv  22268  lply1binom  22314  evl1addd  22345  evl1subd  22346  evl1muld  22347  mamudi  22407  mamudir  22408  1marepvmarrepid  22581  mdetrlin  22608  smadiadetglem1  22677  smadiadetg  22679  cramerimplem1  22689  mat2pmatscmxcl  22746  m2pmfzgsumcl  22754  pmatcollpw  22787  pmatcollpwfi  22788  pmatcollpw3fi1lem1  22792  cpmidpmatlem2  22877  cpmadugsumlemF  22882  chcoeffeqlem  22891  ntrin  23069  topssnei  23132  restbas  23166  restntr  23190  cnntri  23279  fiuncmp  23412  nllyrest  23494  nllyidm  23497  hausllycmp  23502  cldllycmp  23503  hauspwdom  23509  txcld  23611  txcn  23634  txlly  23644  txnlly  23645  txhaus  23655  txlm  23656  txkgen  23660  xkococnlem  23667  cnmpt2res  23685  xkoinjcn  23695  basqtop  23719  qtopeu  23724  trfbas2  23851  neifil  23888  hausflim  23989  alexsubALTlem2  24056  cnextfval  24070  cnextfvval  24073  cnextf  24074  cnextfres  24077  clssubg  24117  utop2nei  24259  utop3cls  24260  utopreg  24261  psmetlecl  24325  xmetlecl  24356  prdsxmetlem  24378  bldisj  24408  imasf1obl  24501  prdsbl  24504  stdbdmet  24529  stdbdmopn  24531  met2ndci  24535  metcnp  24554  metustto  24566  metustexhalf  24569  cfilucfil  24572  metucn  24584  lssnlm  24722  nmotri  24760  nmoid  24763  tgioo  24817  blcvx  24819  xrsmopn  24834  reperflem  24840  reconnlem2  24849  opnreen  24853  metdsge  24871  metdsre  24875  metdscnlem  24877  metnrmlem1a  24880  metnrmlem1  24881  metnrmlem3  24883  cncfmet  24935  cnmpopc  24955  icopnfcnv  24973  icopnfhmeo  24974  cnllycmp  24988  evth  24991  lebnumii  24998  nmoleub2lem3  25148  iscfil2  25300  cfil3i  25303  iscfil3  25307  cfilfcls  25308  iscau3  25312  iscmet3lem2  25326  caubl  25342  lmcau  25347  cssbn  25409  rrxcph  25426  minveclem2  25460  pjthlem1  25471  pjthlem2  25472  ivthicc  25493  ovollecl  25518  ovolunlem1a  25531  ovolunnul  25535  ovoliunlem1  25537  ismbl2  25562  nulmbl2  25571  unmbl  25572  volun  25580  voliunlem2  25586  ioombl1lem2  25594  uniioombllem2a  25617  uniioombllem3  25620  uniioombllem4  25621  dyaddisjlem  25630  dyadmaxlem  25632  opnmbllem  25636  volsup2  25640  volcn  25641  ismbfd  25674  mbfi1fseqlem1  25750  mbfi1fseqlem5  25754  itg2lecl  25773  itg2monolem2  25786  itg2gt0  25795  itgspliticc  25872  ellimc3  25914  limcres  25921  dvfval  25932  dvres3  25948  dvres3a  25949  dvmptresicc  25951  dvnff  25959  dvnadd  25965  dvn2bss  25966  dvnres  25967  dvcmul  25981  dvcmulf  25982  dvmptres3  25994  dvmptres2  26000  dvmptntr  26009  dvexp3  26016  dvferm1lem  26022  dvlip  26032  dvlipcn  26033  dvlip2  26034  c1liplem1  26035  dvgt0lem1  26041  dvgt0lem2  26042  dvne0  26050  lhop1lem  26052  lhop2  26054  lhop  26055  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcvx  26059  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  ftc1lem6  26082  ftc1  26083  ftc2ditglem  26086  itgsubstlem  26089  itgpowd  26091  tdeglem4  26099  mdegaddle  26113  mdegmullem  26117  ply1rem  26205  fta1glem2  26208  fta1blem  26210  ig1peu  26214  ig1pdvds  26219  dgrmulc  26311  dgrcolem1  26313  plydivlem4  26338  plydiveu  26340  fta1lem  26349  vieta1lem1  26352  vieta1lem2  26353  plyexmo  26355  taylfvallem1  26398  taylfval  26400  tayl0  26403  taylplem1  26404  taylply2  26409  taylply2OLD  26410  taylply  26411  dvtaylp  26412  dvntaylp  26413  dvntaylp0  26414  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmcaulem  26437  ulmcau  26438  ulmcn  26442  ulmdvlem1  26443  radcnvlem1  26456  radcnvle  26463  psercn  26470  pserdvlem2  26472  pserdv  26473  abelth  26485  tanregt0  26581  dvlog2lem  26694  efopn  26700  logtayllem  26701  logccv  26705  cxplt3  26742  cxpmul2zd  26758  cxpltd  26761  cxpled  26762  cxplt3d  26777  cxple3d  26778  dvsqrt  26784  cxpcn3  26791  cxpaddle  26795  cxpeq  26800  angcan  26845  angvald  26847  ang180lem2  26853  ang180  26857  isosctrlem3  26863  dquartlem1  26894  atantayl2  26981  leibpi  26985  log2tlbnd  26988  birthdaylem3  26996  xrlimcnp  27011  efrlim  27012  efrlimOLD  27013  o1cxp  27018  jensenlem2  27031  jensen  27032  fsumharmonic  27055  lgamucov  27081  lgamcvg2  27098  wilthlem1  27111  basellem3  27126  basellem6  27129  basellem8  27131  ppisval  27147  chtwordi  27199  ppiwordi  27205  mumullem2  27223  mpodvdsmulf1o  27237  dvdsmulf1o  27239  fsumvma  27257  fsumvma2  27258  chpchtsum  27263  chpub  27264  logfacubnd  27265  dchrmulcl  27293  dchrinv  27305  dchrptlem1  27308  dchrptlem2  27309  sumdchr2  27314  dchr2sum  27317  bposlem7  27334  lgslem1  27341  lgslem3  27343  lgsdirprm  27375  lgsqrlem2  27391  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem4  27422  lgseisen  27423  lgsquadlem1  27424  lgsquad2lem1  27428  lgsquad3  27431  m1lgs  27432  2sqlem7  27468  2sq2  27477  2sqmod  27480  chebbnd1lem2  27514  chebbnd1lem3  27515  rplogsumlem1  27528  rpvmasumlem  27531  dchrvmasumlem1  27539  dchrvmasum2lem  27540  dchrvmasumlema  27544  dchrisum0flblem2  27553  dchrisum0fno1  27555  dchrisum0re  27557  logdivsum  27577  pntrsumbnd2  27611  pntpbnd1a  27629  pntpbnd1  27630  pntibndlem2  27635  pntlemr  27646  pntlemj  27647  pntlemf  27649  pnt2  27657  padicabv  27674  ostth2lem2  27678  sltrec  27865  madebday  27938  sltn0  27943  addsproplem6  28007  sleadd1  28022  negsproplem6  28065  mulsproplem13  28154  mulsproplem14  28155  sltmuld  28163  mulsgt0d  28171  halfcut  28416  f1otrg  28879  brbtwn2  28920  colinearalglem2  28922  axcgrtr  28930  axcgrid  28931  axsegconlem7  28938  axsegcon  28942  ax5seglem3  28946  ax5seglem6  28949  ax5seg  28953  axpaschlem  28955  axlowdimlem17  28973  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  axcontlem8  28986  ecgrtg  28998  usgredg2v  29244  vtxdgoddnumeven  29571  2trlond  29959  eupthp1  30235  nmobndi  30794  ubthlem2  30890  ubthlem3  30891  minvecolem2  30894  shuni  31319  pjhthlem1  31410  chscllem2  31657  pjcompi  31691  mayete3i  31747  unoplin  31939  hmoplin  31961  nmophmi  32050  mdslmd4i  32352  isoun  32711  submuladdd  32750  xrge0addcld  32766  xrofsup  32771  eliccelico  32779  elicoelioo  32780  difioo  32784  hashpss  32813  rexdiv  32908  mgcmnt1d  32987  mgcmnt2d  32988  chnub  33002  xrge0addgt0  33022  omndadd2d  33085  omndadd2rd  33086  omndmul2  33089  cycpmcl  33136  cycpm2tr  33139  cyc3evpm  33170  cycpmconjslem2  33175  fldgensdrg  33316  ofldchr  33344  qusker  33377  eqgvscpbl  33378  ringlsmss1  33424  ringlsmss2  33425  lidlmcld  33447  intlidl  33448  lidlunitel  33451  elrspunidl  33456  idlinsubrg  33459  isprmidlc  33475  rhmpreimaprmidl  33479  qsidomlem1  33480  ssdifidllem  33484  mxidlmaxv  33496  mxidlprm  33498  ssmxidllem  33501  opprmxidlabs  33515  qsdrnglem2  33524  resssra  33638  ply1degltdimlem  33673  lindsunlem  33675  fldsdrgfldext  33712  finexttrb  33715  fldgenfldext  33718  fldextrspunlem1  33725  algextdeglem4  33761  algextdeglem8  33765  constrextdg2lem  33789  mdetpmtr2  33823  mdetpmtr12  33824  madjusmdetlem1  33826  madjusmdetlem4  33829  rhmpreimacn  33884  unitdivcld  33900  xrge0mulc1cn  33940  qqhnm  33991  esumcst  34064  esumfsup  34071  esumpmono  34080  esumcvg  34087  difelsiga  34134  sigapisys  34156  sigapildsys  34163  ldgenpisyslem1  34164  1stmbfm  34262  2ndmbfm  34263  dya2icoseg  34279  sibfinima  34341  probmeasb  34432  orvcgteel  34470  orvclteel  34475  ballotlemsima  34518  ballotlemfrceq  34531  sgnmul  34545  ccatmulgnn0dir  34557  fct2relem  34612  ftc2re  34613  chtvalz  34644  subfacp1lem2a  35185  subfaclim  35193  erdsze2lem2  35209  cvmliftlem2  35291  cvmliftlem10  35299  cvmliftlem13  35301  cvmliftiota  35306  cvmlift2lem9  35316  cvmlift2lem11  35318  cvmlift2lem12  35319  cvmliftphtlem  35322  cvmlift3lem6  35329  cvmlift3lem7  35330  cvmlift3lem9  35332  snmlff  35334  mrsubfval  35513  wzel  35825  wsuclem  35826  brsegle  36109  opnregcld  36331  weiunfrlem  36465  fin2so  37614  poimirlem17  37644  poimirlem23  37650  opnmbllem0  37663  mblfinlem3  37666  mblfinlem4  37667  itg2addnclem  37678  itg2addnc  37681  itg2gt0cn  37682  ftc1cnnclem  37698  ftc1cnnc  37699  areacirclem5  37719  indexdom  37741  sstotbnd2  37781  isbnd3  37791  isbnd3b  37792  cntotbnd  37803  ismtyima  37810  heibor1lem  37816  heiborlem8  37825  rrncmslem  37839  reheibor  37846  lkrlsp  39103  lshpkrlem5  39115  ldualssvscl  39159  ldualssvsubcl  39160  llnmlplnN  39541  llncvrlpln  39560  pmapjat1  39855  pclfinN  39902  lautlt  40093  lauteq  40097  lautco  40099  ltrn11  40128  ltrnle  40131  ltrneq2  40150  cdlemednuN  40302  cdleme20k  40321  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme21c  40329  cdleme22e  40346  cdleme22eALTN  40347  cdlemefrs32fva  40402  cdlemg4g  40618  cdlemg18b  40681  cdlemg18c  40682  cdlemj3  40825  dia2dimlem5  41070  dvhopN  41118  cdlemm10N  41120  dihjatcclem4  41423  dochexmidlem2  41463  lclkrlem2o  41523  lcfrlem5  41548  lcfrlem6  41549  lcdlssvscl  41608  mapdpglem6  41680  mapdpglem9  41682  mapdpglem12  41685  mapdpglem14  41687  mapdindp0  41721  hdmaprnlem7N  41857  hdmaprnlem8N  41858  hdmaprnlem3eN  41860  hgmapvvlem3  41927  dvun  42389  addinvcom  42461  evlsaddval  42578  evlsmulval  42579  evladdval  42585  evlmulval  42586  mzpsubst  42759  eldioph2lem1  42771  eldioph2lem2  42772  eldioph2b  42774  diophin  42783  irrapxlem2  42834  irrapxlem4  42836  irrapxlem5  42837  pellexlem1  42840  pellexlem2  42841  pellexlem6  42845  elpell1qr2  42883  pell1qrgaplem  42884  pell1qrgap  42885  pellqrex  42890  pellfundex  42897  pellfund14  42909  rmspecsqrtnq  42917  rmxyadd  42933  congsub  42982  mzpcong  42984  congrep  42985  acongtr  42990  acongrep  42992  jm2.19lem1  43001  jm2.22  43007  jm2.23  43008  jm2.26lem3  43013  jm2.26  43014  jm2.27a  43017  fnwe2lem2  43063  aomclem6  43071  hbtlem2  43136  hbtlem4  43138  hbtlem5  43140  dgraa0p  43161  rngunsnply  43181  proot1hash  43207  nnoeomeqom  43325  cantnf2  43338  omabs2  43345  naddcnff  43375  naddcnffo  43377  naddcnfcom  43379  naddcnfid1  43380  expgrowth  44354  fpmd  45270  abslt2sqd  45371  ioondisj2  45506  ioondisj1  45507  eliocre  45522  ioossioobi  45530  iooiinicc  45555  iooiinioc  45569  icossico2  45577  lptioo2  45646  limcresiooub  45657  limsupequzlem  45737  xlimmnfvlem2  45848  xlimpnfvlem2  45852  cncfuni  45901  cncfiooicclem1  45908  cxpcncf2  45914  dvcnre  45931  dvresntr  45933  dvresioo  45936  dvbdfbdioolem1  45943  dvnmptdivc  45953  dvnxpaek  45957  itgsinexplem1  45969  itgcoscmulx  45984  itgiccshift  45995  itgperiod  45996  ovolsplit  46003  stoweidlem11  46026  stoweidlem26  46041  stoweidlem34  46049  stoweidlem36  46051  stoweidlem38  46053  stirlinglem5  46093  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem20  46142  fourierdlem58  46179  fourierdlem72  46193  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem79  46200  fourierdlem80  46201  fourierdlem87  46208  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem113  46234  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  etransclem46  46295  etransclem47  46296  rrndistlt  46305  rrnprjdstle  46316  ioorrnopnxrlem  46321  sge0ssre  46412  sge0seq  46461  hsphoidmvle2  46600  hsphoidmvle  46601  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmvlelem1  46610  hoidifhspdmvle  46635  hoiqssbllem2  46638  ovolval5lem2  46668  iinhoiicc  46689  iunhoiioo  46691  vonioolem2  46696  vonicclem2  46699  issmflem  46742  submodlt  47352  iccpartdisj  47424  m1expevenALTV  47634  fpprel2  47728  tgoldbach  47804  opstrgric  47895  gpg3kgrtriex  48045  nn0eo  48449  fdivpm  48464  refdivpm  48465  elbigolo1  48478  logbpw2m1  48488  fllog2  48489  dignn0flhalflem1  48536  dignn0flhalflem2  48537  itsclinecirc0in  48696  2itscplem2  48700  itscnhlinecirc02plem1  48703  iccdisj2  48795