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  4815  fr2nr  5601  soltmin  6093  f1oprg  6820  f1prex  7230  fveqf1o  7248  weniso  7300  fr3nr  7717  suppofssd  8145  smogt  8299  smocdmdom  8300  oacomf1o  8492  en2prd  8984  difsnen  8987  enfixsn  9014  domss2  9064  ssenen  9079  marypha1lem  9336  fisupcl  9373  ordtypelem3  9425  ordtypelem8  9430  oieu  9444  oismo  9445  wofib  9450  wemaplem2  9452  wemapso  9456  wemapso2lem  9457  unxpwdom2  9493  infdifsn  9566  oemapvali  9593  cantnflem1c  9596  cantnflem1  9598  cantnf  9602  cnfcom3  9613  r1ordg  9690  dif1card  9920  infxpenlem  9923  dfac8clem  9942  infxp  10124  infmap2  10127  cflim2  10173  coftr  10183  fin2i2  10228  enfin2i  10231  fin23lem26  10235  fin23lem27  10238  fin23lem40  10261  isf32lem2  10264  isf32lem3  10265  isf32lem4  10266  isf32lem7  10269  isf32lem9  10271  fin1a2lem13  10322  fin12  10323  alephexp1  10490  gchdomtri  10540  fpwwe2lem11  10552  fpwwe2lem12  10553  gchpwdom  10581  gchhar  10590  adderpqlem  10865  mulerpqlem  10866  addassnq  10869  mulassnq  10870  distrnq  10872  mulidnq  10874  recmulnq  10875  ltexnq  10886  distrlem1pr  10936  distrlem4pr  10937  prlem936  10958  reclem3pr  10960  mulcmpblnr  10982  mulgt0d  11288  mul4d  11345  add4d  11362  add42d  11363  subcan  11436  addsub4d  11539  subadd4d  11540  sub4d  11541  2addsubd  11542  addsubeq4d  11543  muladdd  11595  mulsubd  11596  addgegt0d  11710  addgtge0d  11711  addge0d  11713  mulge0d  11714  le2subd  11757  ltleaddd  11758  leltaddd  11759  lt2subd  11761  divdivdiv  11842  divcan5  11843  divne0d  11933  recdivd  11934  recdiv2d  11935  divcan6d  11936  ddcand  11937  rec11d  11938  divmuldivd  11958  divmul13d  11959  divmul24d  11960  divadddivd  11961  divsubdivd  11962  divmuleqd  11963  divdivdivd  11964  mulge0b  12012  recreclt  12041  divgt0d  12077  mulgt1d  12078  lemulge11d  12079  lemulge12d  12080  ltmul12ad  12083  lemul12ad  12084  lemul12bd  12085  supmul1  12111  nndivtr  12192  qreccl  12882  ledivdivd  12974  lediv12ad  13008  lt2mul2divd  13018  xlt2add  13175  supxrun  13231  supxrre  13242  infxrre  13252  elicore  13314  iccss2  13333  iccssico2  13336  icossico2d  13337  lincmb01cmp  13411  iccf1o  13412  fzrev2i  13505  2tnp1ge0ge0  13749  m1modnnsub1  13840  modaddmodup  13857  modaddmodlo  13858  modsubdir  13863  fzennn  13891  sermono  13957  mulexpz  14025  expaddz  14029  sqdiv  14044  expsubd  14080  ltexp2a  14089  expmordi  14090  leexp2a  14095  expmulnbnd  14158  digit1  14160  lt2sqd  14179  le2sqd  14180  sq11d  14181  bcm1k  14238  bcp1n  14239  bcp1nk  14240  hashf1lem1  14378  cshw1  14745  2swrd2eqwrdeq  14876  ofccat  14892  absrele  15231  sqreulem  15283  sqrtmuld  15348  sqrtsq2d  15349  sqrtled  15350  sqrtltd  15351  sqr11d  15352  abs3lemd  15387  rlimuni  15473  climuni  15475  lo1resb  15487  o1resb  15489  2clim  15495  addcn2  15517  mulcn2  15519  o1of2  15536  o1rlimmul  15542  lo1add  15550  lo1mul  15551  isercolllem1  15588  caucvgrlem  15596  iseraltlem2  15606  iseraltlem3  15607  mptfzshft  15701  fsumrev  15702  fsum0diag2  15706  binomlem  15752  climcndslem1  15772  climcndslem2  15773  harmonic  15782  mertenslem1  15807  fprodser  15872  fprodrev  15900  efcllem  16000  moddvds  16190  dvds1  16246  dvdsext  16248  evennn2n  16278  bitsinv1  16369  sadaddlem  16393  sadasslem  16397  sadeq  16399  mulgcd  16475  dvdssqlem  16493  lcmftp  16563  rpmulgcd2  16583  coprmproddvdslem  16589  isprm5  16634  isprm6  16641  crth  16705  eulerthlem2  16709  prmdiveq  16713  pythagtriplem11  16753  pythagtriplem13  16755  pcgcd1  16805  pcprmpw2  16810  pcaddlem  16816  fldivp1  16825  4sqlem12  16884  4sqlem14  16886  4sqlem15  16887  4sqlem16  16888  vdwapun  16902  mreexexlem4d  17570  acsfn1  17584  acsfn2  17586  sscpwex  17739  rescabs  17757  yonedainv  18204  chnub  18545  subm0  18740  pmtrfb  19394  psgnunilem1  19422  odmodnn0  19469  odeq  19479  dfod2  19493  sylow1lem1  19527  lsmsubg  19583  lsmmod  19604  lsmdisj2  19611  ghmplusg  19775  odadd  19779  gexexlem  19781  lt6abl  19824  cyggex2  19826  dprdfinv  19950  dmdprdsplitlem  19968  dpjidcl  19989  ablfacrp  19997  ablfacrp2  19998  ablfac1c  20002  ablfac1eu  20004  omndadd2d  20059  omndadd2rd  20060  omndmul2  20062  acsfn1p  20732  lcomfsupp  20853  lssvancl1  20896  lssvnegcl  20907  lspprvacl  20950  ellspsni  20952  lspsn  20953  lmhmplusg  20996  lmhmima  20999  lmhmpreima  21000  reslmhm  21004  lbsind2  21033  lsmcl  21035  lsmelval2  21037  lsppreli  21042  lspprabs  21047  pj1lmhm  21052  lssvs0or  21065  lspabs3  21076  lspfixed  21083  lspexch  21084  lsmcv  21096  lspsolv  21098  drngnidl  21198  rhmpreimaidl  21232  rngqiprngimfo  21256  rngqiprngfulem4  21269  gzrngunit  21388  zringlpirlem3  21419  prmirredlem  21427  znf1o  21506  znunithash  21519  freshmansdream  21529  ofldchr  21531  frlmsubgval  21720  frlmvplusgvalc  21722  frlmvscaval  21723  frlmphllem  21735  frlmphl  21736  frlmssuvc1  21749  frlmsslsp  21751  frlmup1  21753  frlmup2  21754  lindfind2  21773  lindfrn  21776  f1lindf  21777  islindf4  21793  mplbas2  21997  evlslem3  22035  evlslem1  22037  evladdval  22058  evlmulval  22059  coe1addfv  22207  lply1binom  22254  evl1addd  22285  evl1subd  22286  evl1muld  22287  mamudi  22347  mamudir  22348  1marepvmarrepid  22519  mdetrlin  22546  smadiadetglem1  22615  smadiadetg  22617  cramerimplem1  22627  mat2pmatscmxcl  22684  m2pmfzgsumcl  22692  pmatcollpw  22725  pmatcollpwfi  22726  pmatcollpw3fi1lem1  22730  cpmidpmatlem2  22815  cpmadugsumlemF  22820  chcoeffeqlem  22829  ntrin  23005  topssnei  23068  restbas  23102  restntr  23126  cnntri  23215  fiuncmp  23348  nllyrest  23430  nllyidm  23433  hausllycmp  23438  cldllycmp  23439  hauspwdom  23445  txcld  23547  txcn  23570  txlly  23580  txnlly  23581  txhaus  23591  txlm  23592  txkgen  23596  xkococnlem  23603  cnmpt2res  23621  xkoinjcn  23631  basqtop  23655  qtopeu  23660  trfbas2  23787  neifil  23824  hausflim  23925  alexsubALTlem2  23992  cnextfval  24006  cnextfvval  24009  cnextf  24010  cnextfres  24013  clssubg  24053  utop2nei  24194  utop3cls  24195  utopreg  24196  psmetlecl  24259  xmetlecl  24290  prdsxmetlem  24312  bldisj  24342  imasf1obl  24432  prdsbl  24435  stdbdmet  24460  stdbdmopn  24462  met2ndci  24466  metcnp  24485  metustto  24497  metustexhalf  24500  cfilucfil  24503  metucn  24515  lssnlm  24645  nmotri  24683  nmoid  24686  tgioo  24740  blcvx  24742  xrsmopn  24757  reperflem  24763  reconnlem2  24772  opnreen  24776  metdsge  24794  metdsre  24798  metdscnlem  24800  metnrmlem1a  24803  metnrmlem1  24804  metnrmlem3  24806  cncfmet  24858  cnmpopc  24878  icopnfcnv  24896  icopnfhmeo  24897  cnllycmp  24911  evth  24914  lebnumii  24921  nmoleub2lem3  25071  iscfil2  25222  cfil3i  25225  iscfil3  25229  cfilfcls  25230  iscau3  25234  iscmet3lem2  25248  caubl  25264  lmcau  25269  cssbn  25331  rrxcph  25348  minveclem2  25382  pjthlem1  25393  pjthlem2  25394  ivthicc  25415  ovollecl  25440  ovolunlem1a  25453  ovolunnul  25457  ovoliunlem1  25459  ismbl2  25484  nulmbl2  25493  unmbl  25494  volun  25502  voliunlem2  25508  ioombl1lem2  25516  uniioombllem2a  25539  uniioombllem3  25542  uniioombllem4  25543  dyaddisjlem  25552  dyadmaxlem  25554  opnmbllem  25558  volsup2  25562  volcn  25563  ismbfd  25596  mbfi1fseqlem1  25672  mbfi1fseqlem5  25676  itg2lecl  25695  itg2monolem2  25708  itg2gt0  25717  itgspliticc  25794  ellimc3  25836  limcres  25843  dvfval  25854  dvres3  25870  dvres3a  25871  dvmptresicc  25873  dvnff  25881  dvnadd  25887  dvn2bss  25888  dvnres  25889  dvcmul  25903  dvcmulf  25904  dvmptres3  25916  dvmptres2  25922  dvmptntr  25931  dvexp3  25938  dvferm1lem  25944  dvlip  25954  dvlipcn  25955  dvlip2  25956  c1liplem1  25957  dvgt0lem1  25963  dvgt0lem2  25964  dvne0  25972  lhop1lem  25974  lhop2  25976  lhop  25977  dvcnvrelem1  25978  dvcnvrelem2  25979  dvcvx  25981  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  ftc1lem6  26004  ftc1  26005  ftc2ditglem  26008  itgsubstlem  26011  itgpowd  26013  tdeglem4  26021  mdegaddle  26035  mdegmullem  26039  ply1rem  26127  fta1glem2  26130  fta1blem  26132  ig1peu  26136  ig1pdvds  26141  dgrmulc  26233  dgrcolem1  26235  plydivlem4  26260  plydiveu  26262  fta1lem  26271  vieta1lem1  26274  vieta1lem2  26275  plyexmo  26277  taylfvallem1  26320  taylfval  26322  tayl0  26325  taylplem1  26326  taylply2  26331  taylply2OLD  26332  taylply  26333  dvtaylp  26334  dvntaylp  26335  dvntaylp0  26336  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  ulmdvlem1  26365  radcnvlem1  26378  radcnvle  26385  psercn  26392  pserdvlem2  26394  pserdv  26395  abelth  26407  tanregt0  26504  dvlog2lem  26617  efopn  26623  logtayllem  26624  logccv  26628  cxplt3  26665  cxpmul2zd  26681  cxpltd  26684  cxpled  26685  cxplt3d  26700  cxple3d  26701  dvsqrt  26707  cxpcn3  26714  cxpaddle  26718  cxpeq  26723  angcan  26768  angvald  26770  ang180lem2  26776  ang180  26780  isosctrlem3  26786  dquartlem1  26817  atantayl2  26904  leibpi  26908  log2tlbnd  26911  birthdaylem3  26919  xrlimcnp  26934  efrlim  26935  efrlimOLD  26936  o1cxp  26941  jensenlem2  26954  jensen  26955  fsumharmonic  26978  lgamucov  27004  lgamcvg2  27021  wilthlem1  27034  basellem3  27049  basellem6  27052  basellem8  27054  ppisval  27070  chtwordi  27122  ppiwordi  27128  mumullem2  27146  mpodvdsmulf1o  27160  dvdsmulf1o  27162  fsumvma  27180  fsumvma2  27181  chpchtsum  27186  chpub  27187  logfacubnd  27188  dchrmulcl  27216  dchrinv  27228  dchrptlem1  27231  dchrptlem2  27232  sumdchr2  27237  dchr2sum  27240  bposlem7  27257  lgslem1  27264  lgslem3  27266  lgsdirprm  27298  lgsqrlem2  27314  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem4  27345  lgseisen  27346  lgsquadlem1  27347  lgsquad2lem1  27351  lgsquad3  27354  m1lgs  27355  2sqlem7  27391  2sq2  27400  2sqmod  27403  chebbnd1lem2  27437  chebbnd1lem3  27438  rplogsumlem1  27451  rpvmasumlem  27454  dchrvmasumlem1  27462  dchrvmasum2lem  27463  dchrvmasumlema  27467  dchrisum0flblem2  27476  dchrisum0fno1  27478  dchrisum0re  27480  logdivsum  27500  pntrsumbnd2  27534  pntpbnd1a  27552  pntpbnd1  27553  pntibndlem2  27558  pntlemr  27569  pntlemj  27570  pntlemf  27572  pnt2  27580  padicabv  27597  ostth2lem2  27601  lesrecd  27796  ltsrecd  27798  madebday  27896  addsproplem6  27970  negsproplem6  28029  mulsproplem13  28124  mulsproplem14  28125  ltmulsd  28133  mulsgt0d  28141  f1otrg  28943  brbtwn2  28978  colinearalglem2  28980  axcgrtr  28988  axcgrid  28989  axsegconlem7  28996  axsegcon  29000  ax5seglem3  29004  ax5seglem6  29007  ax5seg  29011  axpaschlem  29013  axlowdimlem17  29031  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  ecgrtg  29056  usgredg2v  29300  vtxdgoddnumeven  29627  2trlond  30012  eupthp1  30291  nmobndi  30850  ubthlem2  30946  ubthlem3  30947  minvecolem2  30950  shuni  31375  pjhthlem1  31466  chscllem2  31713  pjcompi  31747  mayete3i  31803  unoplin  31995  hmoplin  32017  nmophmi  32106  mdslmd4i  32408  isoun  32781  submuladdd  32819  receqid  32824  xrge0addcld  32842  xrofsup  32847  eliccelico  32857  elicoelioo  32858  difioo  32862  hashpss  32889  sgnmul  32916  rexdiv  33007  mgcmnt1d  33079  mgcmnt2d  33080  xrge0addgt0  33099  cycpmcl  33198  cycpm2tr  33201  cyc3evpm  33232  cycpmconjslem2  33237  fldgensdrg  33396  qusker  33430  eqgvscpbl  33431  ringlsmss1  33477  ringlsmss2  33478  lidlmcld  33500  intlidl  33501  lidlunitel  33504  elrspunidl  33509  idlinsubrg  33512  isprmidlc  33528  rhmpreimaprmidl  33532  qsidomlem1  33533  ssdifidllem  33537  mxidlmaxv  33549  mxidlprm  33551  ssmxidllem  33554  opprmxidlabs  33568  qsdrnglem2  33577  mplvrpmmhm  33711  mplvrpmrhm  33712  esplyind  33731  resssra  33743  ply1degltdimlem  33779  lindsunlem  33781  sdrgfldext  33807  fldsdrgfldext  33818  finexttrb  33822  fldgenfldext  33825  fldextrspunlem1  33832  algextdeglem4  33877  algextdeglem8  33881  constrextdg2lem  33905  mdetpmtr2  33981  mdetpmtr12  33982  madjusmdetlem1  33984  madjusmdetlem4  33987  rhmpreimacn  34042  unitdivcld  34058  xrge0mulc1cn  34098  qqhnm  34147  esumcst  34220  esumfsup  34227  esumpmono  34236  esumcvg  34243  difelsiga  34290  sigapisys  34312  sigapildsys  34319  ldgenpisyslem1  34320  1stmbfm  34417  2ndmbfm  34418  dya2icoseg  34434  sibfinima  34496  probmeasb  34587  orvcgteel  34625  orvclteel  34630  ballotlemsima  34673  ballotlemfrceq  34686  ccatmulgnn0dir  34699  fct2relem  34754  ftc2re  34755  chtvalz  34786  r1filimi  35259  subfacp1lem2a  35374  subfaclim  35382  erdsze2lem2  35398  cvmliftlem2  35480  cvmliftlem10  35488  cvmliftlem13  35490  cvmliftiota  35495  cvmlift2lem9  35505  cvmlift2lem11  35507  cvmlift2lem12  35508  cvmliftphtlem  35511  cvmlift3lem6  35518  cvmlift3lem7  35519  cvmlift3lem9  35521  snmlff  35523  mrsubfval  35702  wzel  36016  wsuclem  36017  brsegle  36302  opnregcld  36524  weiunfrlem  36658  fin2so  37808  poimirlem17  37838  poimirlem23  37844  opnmbllem0  37857  mblfinlem3  37860  mblfinlem4  37861  itg2addnclem  37872  itg2addnc  37875  itg2gt0cn  37876  ftc1cnnclem  37892  ftc1cnnc  37893  areacirclem5  37913  indexdom  37935  sstotbnd2  37975  isbnd3  37985  isbnd3b  37986  cntotbnd  37997  ismtyima  38004  heibor1lem  38010  heiborlem8  38019  rrncmslem  38033  reheibor  38040  lkrlsp  39362  lshpkrlem5  39374  ldualssvscl  39418  ldualssvsubcl  39419  llnmlplnN  39799  llncvrlpln  39818  pmapjat1  40113  pclfinN  40160  lautlt  40351  lauteq  40355  lautco  40357  ltrn11  40386  ltrnle  40389  ltrneq2  40408  cdlemednuN  40560  cdleme20k  40579  cdleme20l2  40581  cdleme20l  40582  cdleme20m  40583  cdleme21c  40587  cdleme22e  40604  cdleme22eALTN  40605  cdlemefrs32fva  40660  cdlemg4g  40876  cdlemg18b  40939  cdlemg18c  40940  cdlemj3  41083  dia2dimlem5  41328  dvhopN  41376  cdlemm10N  41378  dihjatcclem4  41681  dochexmidlem2  41721  lclkrlem2o  41781  lcfrlem5  41806  lcfrlem6  41807  lcdlssvscl  41866  mapdpglem6  41938  mapdpglem9  41940  mapdpglem12  41943  mapdpglem14  41945  mapdindp0  41979  hdmaprnlem7N  42115  hdmaprnlem8N  42116  hdmaprnlem3eN  42118  hgmapvvlem3  42185  dvun  42614  addinvcom  42687  evlsaddval  42814  evlsmulval  42815  mzpsubst  42990  eldioph2lem1  43002  eldioph2lem2  43003  eldioph2b  43005  diophin  43014  irrapxlem2  43065  irrapxlem4  43067  irrapxlem5  43068  pellexlem1  43071  pellexlem2  43072  pellexlem6  43076  elpell1qr2  43114  pell1qrgaplem  43115  pell1qrgap  43116  pellqrex  43121  pellfundex  43128  pellfund14  43140  rmspecsqrtnq  43148  rmxyadd  43163  congsub  43212  mzpcong  43214  congrep  43215  acongtr  43220  acongrep  43222  jm2.19lem1  43231  jm2.22  43237  jm2.23  43238  jm2.26lem3  43243  jm2.26  43244  jm2.27a  43247  fnwe2lem2  43293  aomclem6  43301  hbtlem2  43366  hbtlem4  43368  hbtlem5  43370  dgraa0p  43391  rngunsnply  43411  proot1hash  43437  nnoeomeqom  43554  cantnf2  43567  omabs2  43574  naddcnff  43604  naddcnffo  43606  naddcnfcom  43608  naddcnfid1  43609  expgrowth  44576  fpmd  45507  abslt2sqd  45605  ioondisj2  45739  ioondisj1  45740  eliocre  45755  ioossioobi  45763  iooiinicc  45788  iooiinioc  45802  lptioo2  45877  limcresiooub  45886  limsupequzlem  45966  xlimmnfvlem2  46077  xlimpnfvlem2  46081  cncfuni  46130  cncfiooicclem1  46137  cxpcncf2  46143  dvcnre  46160  dvresntr  46162  dvresioo  46165  dvbdfbdioolem1  46172  dvnmptdivc  46182  dvnxpaek  46186  itgsinexplem1  46198  itgcoscmulx  46213  itgiccshift  46224  itgperiod  46225  ovolsplit  46232  stoweidlem11  46255  stoweidlem26  46270  stoweidlem34  46278  stoweidlem36  46280  stoweidlem38  46282  stirlinglem5  46322  dirkercncflem2  46348  dirkercncflem4  46350  fourierdlem20  46371  fourierdlem58  46408  fourierdlem72  46422  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem79  46429  fourierdlem80  46430  fourierdlem87  46437  fourierdlem94  46444  fourierdlem103  46453  fourierdlem104  46454  fourierdlem107  46457  fourierdlem113  46463  sqwvfoura  46472  sqwvfourb  46473  fourierswlem  46474  fouriersw  46475  etransclem46  46524  etransclem47  46525  rrndistlt  46534  rrnprjdstle  46545  ioorrnopnxrlem  46550  sge0ssre  46641  sge0seq  46690  hsphoidmvle2  46829  hsphoidmvle  46830  hoidmv1lelem1  46835  hoidmv1lelem2  46836  hoidmv1lelem3  46837  hoidmvlelem1  46839  hoidifhspdmvle  46864  hoiqssbllem2  46867  ovolval5lem2  46897  iinhoiicc  46918  iunhoiioo  46920  vonioolem2  46925  vonicclem2  46928  issmflem  46971  submodlt  47596  iccpartdisj  47683  m1expevenALTV  47893  fpprel2  47987  tgoldbach  48063  opstrgric  48172  gpg3kgrtriex  48335  nn0eo  48774  fdivpm  48789  refdivpm  48790  elbigolo1  48803  logbpw2m1  48813  fllog2  48814  dignn0flhalflem1  48861  dignn0flhalflem2  48862  itsclinecirc0in  49021  2itscplem2  49025  itscnhlinecirc02plem1  49028  iccdisj2  49142