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  4817  fr2nr  5609  soltmin  6101  f1oprg  6828  f1prex  7240  fveqf1o  7258  weniso  7310  fr3nr  7727  suppofssd  8155  smogt  8309  smocdmdom  8310  oacomf1o  8502  en2prd  8996  difsnen  8999  enfixsn  9026  domss2  9076  ssenen  9091  marypha1lem  9348  fisupcl  9385  ordtypelem3  9437  ordtypelem8  9442  oieu  9456  oismo  9457  wofib  9462  wemaplem2  9464  wemapso  9468  wemapso2lem  9469  unxpwdom2  9505  infdifsn  9578  oemapvali  9605  cantnflem1c  9608  cantnflem1  9610  cantnf  9614  cnfcom3  9625  r1ordg  9702  dif1card  9932  infxpenlem  9935  dfac8clem  9954  infxp  10136  infmap2  10139  cflim2  10185  coftr  10195  fin2i2  10240  enfin2i  10243  fin23lem26  10247  fin23lem27  10250  fin23lem40  10273  isf32lem2  10276  isf32lem3  10277  isf32lem4  10278  isf32lem7  10281  isf32lem9  10283  fin1a2lem13  10334  fin12  10335  alephexp1  10502  gchdomtri  10552  fpwwe2lem11  10564  fpwwe2lem12  10565  gchpwdom  10593  gchhar  10602  adderpqlem  10877  mulerpqlem  10878  addassnq  10881  mulassnq  10882  distrnq  10884  mulidnq  10886  recmulnq  10887  ltexnq  10898  distrlem1pr  10948  distrlem4pr  10949  prlem936  10970  reclem3pr  10972  mulcmpblnr  10994  mulgt0d  11300  mul4d  11357  add4d  11374  add42d  11375  subcan  11448  addsub4d  11551  subadd4d  11552  sub4d  11553  2addsubd  11554  addsubeq4d  11555  muladdd  11607  mulsubd  11608  addgegt0d  11722  addgtge0d  11723  addge0d  11725  mulge0d  11726  le2subd  11769  ltleaddd  11770  leltaddd  11771  lt2subd  11773  divdivdiv  11854  divcan5  11855  divne0d  11945  recdivd  11946  recdiv2d  11947  divcan6d  11948  ddcand  11949  rec11d  11950  divmuldivd  11970  divmul13d  11971  divmul24d  11972  divadddivd  11973  divsubdivd  11974  divmuleqd  11975  divdivdivd  11976  mulge0b  12024  recreclt  12053  divgt0d  12089  mulgt1d  12090  lemulge11d  12091  lemulge12d  12092  ltmul12ad  12095  lemul12ad  12096  lemul12bd  12097  supmul1  12123  nndivtr  12204  qreccl  12894  ledivdivd  12986  lediv12ad  13020  lt2mul2divd  13030  xlt2add  13187  supxrun  13243  supxrre  13254  infxrre  13264  elicore  13326  iccss2  13345  iccssico2  13348  icossico2d  13349  lincmb01cmp  13423  iccf1o  13424  fzrev2i  13517  2tnp1ge0ge0  13761  m1modnnsub1  13852  modaddmodup  13869  modaddmodlo  13870  modsubdir  13875  fzennn  13903  sermono  13969  mulexpz  14037  expaddz  14041  sqdiv  14056  expsubd  14092  ltexp2a  14101  expmordi  14102  leexp2a  14107  expmulnbnd  14170  digit1  14172  lt2sqd  14191  le2sqd  14192  sq11d  14193  bcm1k  14250  bcp1n  14251  bcp1nk  14252  hashf1lem1  14390  cshw1  14757  2swrd2eqwrdeq  14888  ofccat  14904  absrele  15243  sqreulem  15295  sqrtmuld  15360  sqrtsq2d  15361  sqrtled  15362  sqrtltd  15363  sqr11d  15364  abs3lemd  15399  rlimuni  15485  climuni  15487  lo1resb  15499  o1resb  15501  2clim  15507  addcn2  15529  mulcn2  15531  o1of2  15548  o1rlimmul  15554  lo1add  15562  lo1mul  15563  isercolllem1  15600  caucvgrlem  15608  iseraltlem2  15618  iseraltlem3  15619  mptfzshft  15713  fsumrev  15714  fsum0diag2  15718  binomlem  15764  climcndslem1  15784  climcndslem2  15785  harmonic  15794  mertenslem1  15819  fprodser  15884  fprodrev  15912  efcllem  16012  moddvds  16202  dvds1  16258  dvdsext  16260  evennn2n  16290  bitsinv1  16381  sadaddlem  16405  sadasslem  16409  sadeq  16411  mulgcd  16487  dvdssqlem  16505  lcmftp  16575  rpmulgcd2  16595  coprmproddvdslem  16601  isprm5  16646  isprm6  16653  crth  16717  eulerthlem2  16721  prmdiveq  16725  pythagtriplem11  16765  pythagtriplem13  16767  pcgcd1  16817  pcprmpw2  16822  pcaddlem  16828  fldivp1  16837  4sqlem12  16896  4sqlem14  16898  4sqlem15  16899  4sqlem16  16900  vdwapun  16914  mreexexlem4d  17582  acsfn1  17596  acsfn2  17598  sscpwex  17751  rescabs  17769  yonedainv  18216  chnub  18557  subm0  18752  pmtrfb  19406  psgnunilem1  19434  odmodnn0  19481  odeq  19491  dfod2  19505  sylow1lem1  19539  lsmsubg  19595  lsmmod  19616  lsmdisj2  19623  ghmplusg  19787  odadd  19791  gexexlem  19793  lt6abl  19836  cyggex2  19838  dprdfinv  19962  dmdprdsplitlem  19980  dpjidcl  20001  ablfacrp  20009  ablfacrp2  20010  ablfac1c  20014  ablfac1eu  20016  omndadd2d  20071  omndadd2rd  20072  omndmul2  20074  acsfn1p  20744  lcomfsupp  20865  lssvancl1  20908  lssvnegcl  20919  lspprvacl  20962  ellspsni  20964  lspsn  20965  lmhmplusg  21008  lmhmima  21011  lmhmpreima  21012  reslmhm  21016  lbsind2  21045  lsmcl  21047  lsmelval2  21049  lsppreli  21054  lspprabs  21059  pj1lmhm  21064  lssvs0or  21077  lspabs3  21088  lspfixed  21095  lspexch  21096  lsmcv  21108  lspsolv  21110  drngnidl  21210  rhmpreimaidl  21244  rngqiprngimfo  21268  rngqiprngfulem4  21281  gzrngunit  21400  zringlpirlem3  21431  prmirredlem  21439  znf1o  21518  znunithash  21531  freshmansdream  21541  ofldchr  21543  frlmsubgval  21732  frlmvplusgvalc  21734  frlmvscaval  21735  frlmphllem  21747  frlmphl  21748  frlmssuvc1  21761  frlmsslsp  21763  frlmup1  21765  frlmup2  21766  lindfind2  21785  lindfrn  21788  f1lindf  21789  islindf4  21805  mplbas2  22009  evlslem3  22047  evlslem1  22049  evladdval  22070  evlmulval  22071  coe1addfv  22219  lply1binom  22266  evl1addd  22297  evl1subd  22298  evl1muld  22299  mamudi  22359  mamudir  22360  1marepvmarrepid  22531  mdetrlin  22558  smadiadetglem1  22627  smadiadetg  22629  cramerimplem1  22639  mat2pmatscmxcl  22696  m2pmfzgsumcl  22704  pmatcollpw  22737  pmatcollpwfi  22738  pmatcollpw3fi1lem1  22742  cpmidpmatlem2  22827  cpmadugsumlemF  22832  chcoeffeqlem  22841  ntrin  23017  topssnei  23080  restbas  23114  restntr  23138  cnntri  23227  fiuncmp  23360  nllyrest  23442  nllyidm  23445  hausllycmp  23450  cldllycmp  23451  hauspwdom  23457  txcld  23559  txcn  23582  txlly  23592  txnlly  23593  txhaus  23603  txlm  23604  txkgen  23608  xkococnlem  23615  cnmpt2res  23633  xkoinjcn  23643  basqtop  23667  qtopeu  23672  trfbas2  23799  neifil  23836  hausflim  23937  alexsubALTlem2  24004  cnextfval  24018  cnextfvval  24021  cnextf  24022  cnextfres  24025  clssubg  24065  utop2nei  24206  utop3cls  24207  utopreg  24208  psmetlecl  24271  xmetlecl  24302  prdsxmetlem  24324  bldisj  24354  imasf1obl  24444  prdsbl  24447  stdbdmet  24472  stdbdmopn  24474  met2ndci  24478  metcnp  24497  metustto  24509  metustexhalf  24512  cfilucfil  24515  metucn  24527  lssnlm  24657  nmotri  24695  nmoid  24698  tgioo  24752  blcvx  24754  xrsmopn  24769  reperflem  24775  reconnlem2  24784  opnreen  24788  metdsge  24806  metdsre  24810  metdscnlem  24812  metnrmlem1a  24815  metnrmlem1  24816  metnrmlem3  24818  cncfmet  24870  cnmpopc  24890  icopnfcnv  24908  icopnfhmeo  24909  cnllycmp  24923  evth  24926  lebnumii  24933  nmoleub2lem3  25083  iscfil2  25234  cfil3i  25237  iscfil3  25241  cfilfcls  25242  iscau3  25246  iscmet3lem2  25260  caubl  25276  lmcau  25281  cssbn  25343  rrxcph  25360  minveclem2  25394  pjthlem1  25405  pjthlem2  25406  ivthicc  25427  ovollecl  25452  ovolunlem1a  25465  ovolunnul  25469  ovoliunlem1  25471  ismbl2  25496  nulmbl2  25505  unmbl  25506  volun  25514  voliunlem2  25520  ioombl1lem2  25528  uniioombllem2a  25551  uniioombllem3  25554  uniioombllem4  25555  dyaddisjlem  25564  dyadmaxlem  25566  opnmbllem  25570  volsup2  25574  volcn  25575  ismbfd  25608  mbfi1fseqlem1  25684  mbfi1fseqlem5  25688  itg2lecl  25707  itg2monolem2  25720  itg2gt0  25729  itgspliticc  25806  ellimc3  25848  limcres  25855  dvfval  25866  dvres3  25882  dvres3a  25883  dvmptresicc  25885  dvnff  25893  dvnadd  25899  dvn2bss  25900  dvnres  25901  dvcmul  25915  dvcmulf  25916  dvmptres3  25928  dvmptres2  25934  dvmptntr  25943  dvexp3  25950  dvferm1lem  25956  dvlip  25966  dvlipcn  25967  dvlip2  25968  c1liplem1  25969  dvgt0lem1  25975  dvgt0lem2  25976  dvne0  25984  lhop1lem  25986  lhop2  25988  lhop  25989  dvcnvrelem1  25990  dvcnvrelem2  25991  dvcvx  25993  dvfsumle  25994  dvfsumleOLD  25995  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  ftc1lem6  26016  ftc1  26017  ftc2ditglem  26020  itgsubstlem  26023  itgpowd  26025  tdeglem4  26033  mdegaddle  26047  mdegmullem  26051  ply1rem  26139  fta1glem2  26142  fta1blem  26144  ig1peu  26148  ig1pdvds  26153  dgrmulc  26245  dgrcolem1  26247  plydivlem4  26272  plydiveu  26274  fta1lem  26283  vieta1lem1  26286  vieta1lem2  26287  plyexmo  26289  taylfvallem1  26332  taylfval  26334  tayl0  26337  taylplem1  26338  taylply2  26343  taylply2OLD  26344  taylply  26345  dvtaylp  26346  dvntaylp  26347  dvntaylp0  26348  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmcaulem  26371  ulmcau  26372  ulmcn  26376  ulmdvlem1  26377  radcnvlem1  26390  radcnvle  26397  psercn  26404  pserdvlem2  26406  pserdv  26407  abelth  26419  tanregt0  26516  dvlog2lem  26629  efopn  26635  logtayllem  26636  logccv  26640  cxplt3  26677  cxpmul2zd  26693  cxpltd  26696  cxpled  26697  cxplt3d  26712  cxple3d  26713  dvsqrt  26719  cxpcn3  26726  cxpaddle  26730  cxpeq  26735  angcan  26780  angvald  26782  ang180lem2  26788  ang180  26792  isosctrlem3  26798  dquartlem1  26829  atantayl2  26916  leibpi  26920  log2tlbnd  26923  birthdaylem3  26931  xrlimcnp  26946  efrlim  26947  efrlimOLD  26948  o1cxp  26953  jensenlem2  26966  jensen  26967  fsumharmonic  26990  lgamucov  27016  lgamcvg2  27033  wilthlem1  27046  basellem3  27061  basellem6  27064  basellem8  27066  ppisval  27082  chtwordi  27134  ppiwordi  27140  mumullem2  27158  mpodvdsmulf1o  27172  dvdsmulf1o  27174  fsumvma  27192  fsumvma2  27193  chpchtsum  27198  chpub  27199  logfacubnd  27200  dchrmulcl  27228  dchrinv  27240  dchrptlem1  27243  dchrptlem2  27244  sumdchr2  27249  dchr2sum  27252  bposlem7  27269  lgslem1  27276  lgslem3  27278  lgsdirprm  27310  lgsqrlem2  27326  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem4  27357  lgseisen  27358  lgsquadlem1  27359  lgsquad2lem1  27363  lgsquad3  27366  m1lgs  27367  2sqlem7  27403  2sq2  27412  2sqmod  27415  chebbnd1lem2  27449  chebbnd1lem3  27450  rplogsumlem1  27463  rpvmasumlem  27466  dchrvmasumlem1  27474  dchrvmasum2lem  27475  dchrvmasumlema  27479  dchrisum0flblem2  27488  dchrisum0fno1  27490  dchrisum0re  27492  logdivsum  27512  pntrsumbnd2  27546  pntpbnd1a  27564  pntpbnd1  27565  pntibndlem2  27570  pntlemr  27581  pntlemj  27582  pntlemf  27584  pnt2  27592  padicabv  27609  ostth2lem2  27613  lesrecd  27808  ltsrecd  27810  madebday  27908  addsproplem6  27982  negsproplem6  28041  mulsproplem13  28136  mulsproplem14  28137  ltmulsd  28145  mulsgt0d  28153  f1otrg  28955  brbtwn2  28990  colinearalglem2  28992  axcgrtr  29000  axcgrid  29001  axsegconlem7  29008  axsegcon  29012  ax5seglem3  29016  ax5seglem6  29019  ax5seg  29023  axpaschlem  29025  axlowdimlem17  29043  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  ecgrtg  29068  usgredg2v  29312  vtxdgoddnumeven  29639  2trlond  30024  eupthp1  30303  nmobndi  30863  ubthlem2  30959  ubthlem3  30960  minvecolem2  30963  shuni  31388  pjhthlem1  31479  chscllem2  31726  pjcompi  31760  mayete3i  31816  unoplin  32008  hmoplin  32030  nmophmi  32119  mdslmd4i  32421  isoun  32792  submuladdd  32830  receqid  32835  xrge0addcld  32853  xrofsup  32858  eliccelico  32868  elicoelioo  32869  difioo  32873  hashpss  32900  sgnmul  32927  rexdiv  33018  mgcmnt1d  33090  mgcmnt2d  33091  xrge0addgt0  33110  cycpmcl  33210  cycpm2tr  33213  cyc3evpm  33244  cycpmconjslem2  33249  fldgensdrg  33408  qusker  33442  eqgvscpbl  33443  ringlsmss1  33489  ringlsmss2  33490  lidlmcld  33512  intlidl  33513  lidlunitel  33516  elrspunidl  33521  idlinsubrg  33524  isprmidlc  33540  rhmpreimaprmidl  33544  qsidomlem1  33545  ssdifidllem  33549  mxidlmaxv  33561  mxidlprm  33563  ssmxidllem  33566  opprmxidlabs  33580  qsdrnglem2  33589  mplvrpmmhm  33723  mplvrpmrhm  33724  esplyind  33752  resssra  33764  ply1degltdimlem  33800  lindsunlem  33802  sdrgfldext  33828  fldsdrgfldext  33839  finexttrb  33843  fldgenfldext  33846  fldextrspunlem1  33853  algextdeglem4  33898  algextdeglem8  33902  constrextdg2lem  33926  mdetpmtr2  34002  mdetpmtr12  34003  madjusmdetlem1  34005  madjusmdetlem4  34008  rhmpreimacn  34063  unitdivcld  34079  xrge0mulc1cn  34119  qqhnm  34168  esumcst  34241  esumfsup  34248  esumpmono  34257  esumcvg  34264  difelsiga  34311  sigapisys  34333  sigapildsys  34340  ldgenpisyslem1  34341  1stmbfm  34438  2ndmbfm  34439  dya2icoseg  34455  sibfinima  34517  probmeasb  34608  orvcgteel  34646  orvclteel  34651  ballotlemsima  34694  ballotlemfrceq  34707  ccatmulgnn0dir  34720  fct2relem  34775  ftc2re  34776  chtvalz  34807  r1filimi  35280  subfacp1lem2a  35396  subfaclim  35404  erdsze2lem2  35420  cvmliftlem2  35502  cvmliftlem10  35510  cvmliftlem13  35512  cvmliftiota  35517  cvmlift2lem9  35527  cvmlift2lem11  35529  cvmlift2lem12  35530  cvmliftphtlem  35533  cvmlift3lem6  35540  cvmlift3lem7  35541  cvmlift3lem9  35543  snmlff  35545  mrsubfval  35724  wzel  36038  wsuclem  36039  brsegle  36324  opnregcld  36546  weiunfrlem  36680  fin2so  37858  poimirlem17  37888  poimirlem23  37894  opnmbllem0  37907  mblfinlem3  37910  mblfinlem4  37911  itg2addnclem  37922  itg2addnc  37925  itg2gt0cn  37926  ftc1cnnclem  37942  ftc1cnnc  37943  areacirclem5  37963  indexdom  37985  sstotbnd2  38025  isbnd3  38035  isbnd3b  38036  cntotbnd  38047  ismtyima  38054  heibor1lem  38060  heiborlem8  38069  rrncmslem  38083  reheibor  38090  lkrlsp  39478  lshpkrlem5  39490  ldualssvscl  39534  ldualssvsubcl  39535  llnmlplnN  39915  llncvrlpln  39934  pmapjat1  40229  pclfinN  40276  lautlt  40467  lauteq  40471  lautco  40473  ltrn11  40502  ltrnle  40505  ltrneq2  40524  cdlemednuN  40676  cdleme20k  40695  cdleme20l2  40697  cdleme20l  40698  cdleme20m  40699  cdleme21c  40703  cdleme22e  40720  cdleme22eALTN  40721  cdlemefrs32fva  40776  cdlemg4g  40992  cdlemg18b  41055  cdlemg18c  41056  cdlemj3  41199  dia2dimlem5  41444  dvhopN  41492  cdlemm10N  41494  dihjatcclem4  41797  dochexmidlem2  41837  lclkrlem2o  41897  lcfrlem5  41922  lcfrlem6  41923  lcdlssvscl  41982  mapdpglem6  42054  mapdpglem9  42056  mapdpglem12  42059  mapdpglem14  42061  mapdindp0  42095  hdmaprnlem7N  42231  hdmaprnlem8N  42232  hdmaprnlem3eN  42234  hgmapvvlem3  42301  dvun  42729  addinvcom  42802  evlsaddval  42929  evlsmulval  42930  mzpsubst  43105  eldioph2lem1  43117  eldioph2lem2  43118  eldioph2b  43120  diophin  43129  irrapxlem2  43180  irrapxlem4  43182  irrapxlem5  43183  pellexlem1  43186  pellexlem2  43187  pellexlem6  43191  elpell1qr2  43229  pell1qrgaplem  43230  pell1qrgap  43231  pellqrex  43236  pellfundex  43243  pellfund14  43255  rmspecsqrtnq  43263  rmxyadd  43278  congsub  43327  mzpcong  43329  congrep  43330  acongtr  43335  acongrep  43337  jm2.19lem1  43346  jm2.22  43352  jm2.23  43353  jm2.26lem3  43358  jm2.26  43359  jm2.27a  43362  fnwe2lem2  43408  aomclem6  43416  hbtlem2  43481  hbtlem4  43483  hbtlem5  43485  dgraa0p  43506  rngunsnply  43526  proot1hash  43552  nnoeomeqom  43669  cantnf2  43682  omabs2  43689  naddcnff  43719  naddcnffo  43721  naddcnfcom  43723  naddcnfid1  43724  expgrowth  44691  fpmd  45621  abslt2sqd  45719  ioondisj2  45853  ioondisj1  45854  eliocre  45869  ioossioobi  45877  iooiinicc  45902  iooiinioc  45916  lptioo2  45991  limcresiooub  46000  limsupequzlem  46080  xlimmnfvlem2  46191  xlimpnfvlem2  46195  cncfuni  46244  cncfiooicclem1  46251  cxpcncf2  46257  dvcnre  46274  dvresntr  46276  dvresioo  46279  dvbdfbdioolem1  46286  dvnmptdivc  46296  dvnxpaek  46300  itgsinexplem1  46312  itgcoscmulx  46327  itgiccshift  46338  itgperiod  46339  ovolsplit  46346  stoweidlem11  46369  stoweidlem26  46384  stoweidlem34  46392  stoweidlem36  46394  stoweidlem38  46396  stirlinglem5  46436  dirkercncflem2  46462  dirkercncflem4  46464  fourierdlem20  46485  fourierdlem58  46522  fourierdlem72  46536  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem79  46543  fourierdlem80  46544  fourierdlem87  46551  fourierdlem94  46558  fourierdlem103  46567  fourierdlem104  46568  fourierdlem107  46571  fourierdlem113  46577  sqwvfoura  46586  sqwvfourb  46587  fourierswlem  46588  fouriersw  46589  etransclem46  46638  etransclem47  46639  rrndistlt  46648  rrnprjdstle  46659  ioorrnopnxrlem  46664  sge0ssre  46755  sge0seq  46804  hsphoidmvle2  46943  hsphoidmvle  46944  hoidmv1lelem1  46949  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmvlelem1  46953  hoidifhspdmvle  46978  hoiqssbllem2  46981  ovolval5lem2  47011  iinhoiicc  47032  iunhoiioo  47034  vonioolem2  47039  vonicclem2  47042  issmflem  47085  submodlt  47710  iccpartdisj  47797  m1expevenALTV  48007  fpprel2  48101  tgoldbach  48177  opstrgric  48286  gpg3kgrtriex  48449  nn0eo  48888  fdivpm  48903  refdivpm  48904  elbigolo1  48917  logbpw2m1  48927  fllog2  48928  dignn0flhalflem1  48975  dignn0flhalflem2  48976  itsclinecirc0in  49135  2itscplem2  49139  itscnhlinecirc02plem1  49142  iccdisj2  49256