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  4826  fr2nr  5618  soltmin  6112  f1oprg  6848  f1prex  7262  fveqf1o  7280  weniso  7332  fr3nr  7751  suppofssd  8185  smogt  8339  smocdmdom  8340  oacomf1o  8532  en2prd  9022  enpr2dOLD  9024  difsnen  9027  undomOLD  9034  enfixsn  9055  domss2  9106  ssenen  9121  marypha1lem  9391  fisupcl  9428  ordtypelem3  9480  ordtypelem8  9485  oieu  9499  oismo  9500  wofib  9505  wemaplem2  9507  wemapso  9511  wemapso2lem  9512  unxpwdom2  9548  infdifsn  9617  oemapvali  9644  cantnflem1c  9647  cantnflem1  9649  cantnf  9653  cnfcom3  9664  r1ordg  9738  dif1card  9970  infxpenlem  9973  dfac8clem  9992  infxp  10174  infmap2  10177  cflim2  10223  coftr  10233  fin2i2  10278  enfin2i  10281  fin23lem26  10285  fin23lem27  10288  fin23lem40  10311  isf32lem2  10314  isf32lem3  10315  isf32lem4  10316  isf32lem7  10319  isf32lem9  10321  fin1a2lem13  10372  fin12  10373  alephexp1  10539  gchdomtri  10589  fpwwe2lem11  10601  fpwwe2lem12  10602  gchpwdom  10630  gchhar  10639  adderpqlem  10914  mulerpqlem  10915  addassnq  10918  mulassnq  10919  distrnq  10921  mulidnq  10923  recmulnq  10924  ltexnq  10935  distrlem1pr  10985  distrlem4pr  10986  prlem936  11007  reclem3pr  11009  mulcmpblnr  11031  mulgt0d  11336  mul4d  11393  add4d  11410  add42d  11411  subcan  11484  addsub4d  11587  subadd4d  11588  sub4d  11589  2addsubd  11590  addsubeq4d  11591  muladdd  11643  mulsubd  11644  addgegt0d  11758  addgtge0d  11759  addge0d  11761  mulge0d  11762  le2subd  11805  ltleaddd  11806  leltaddd  11807  lt2subd  11809  divdivdiv  11890  divcan5  11891  divne0d  11981  recdivd  11982  recdiv2d  11983  divcan6d  11984  ddcand  11985  rec11d  11986  divmuldivd  12006  divmul13d  12007  divmul24d  12008  divadddivd  12009  divsubdivd  12010  divmuleqd  12011  divdivdivd  12012  mulge0b  12060  recreclt  12089  divgt0d  12125  mulgt1d  12126  lemulge11d  12127  lemulge12d  12128  ltmul12ad  12131  lemul12ad  12132  lemul12bd  12133  supmul1  12159  nndivtr  12240  qreccl  12935  ledivdivd  13027  lediv12ad  13061  lt2mul2divd  13071  xlt2add  13227  supxrun  13283  supxrre  13294  infxrre  13304  elicore  13366  iccss2  13385  iccssico2  13388  icossico2d  13389  lincmb01cmp  13463  iccf1o  13464  fzrev2i  13557  2tnp1ge0ge0  13798  m1modnnsub1  13889  modaddmodup  13906  modaddmodlo  13907  modsubdir  13912  fzennn  13940  sermono  14006  mulexpz  14074  expaddz  14078  sqdiv  14093  expsubd  14129  ltexp2a  14138  expmordi  14139  leexp2a  14144  expmulnbnd  14207  digit1  14209  lt2sqd  14228  le2sqd  14229  sq11d  14230  bcm1k  14287  bcp1n  14288  bcp1nk  14289  hashf1lem1  14427  cshw1  14794  2swrd2eqwrdeq  14926  ofccat  14942  absrele  15281  sqreulem  15333  sqrtmuld  15398  sqrtsq2d  15399  sqrtled  15400  sqrtltd  15401  sqr11d  15402  abs3lemd  15437  rlimuni  15523  climuni  15525  lo1resb  15537  o1resb  15539  2clim  15545  addcn2  15567  mulcn2  15569  o1of2  15586  o1rlimmul  15592  lo1add  15600  lo1mul  15601  isercolllem1  15638  caucvgrlem  15646  iseraltlem2  15656  iseraltlem3  15657  mptfzshft  15751  fsumrev  15752  fsum0diag2  15756  binomlem  15802  climcndslem1  15822  climcndslem2  15823  harmonic  15832  mertenslem1  15857  fprodser  15922  fprodrev  15950  efcllem  16050  moddvds  16240  dvds1  16296  dvdsext  16298  evennn2n  16328  bitsinv1  16419  sadaddlem  16443  sadasslem  16447  sadeq  16449  mulgcd  16525  dvdssqlem  16543  lcmftp  16613  rpmulgcd2  16633  coprmproddvdslem  16639  isprm5  16684  isprm6  16691  crth  16755  eulerthlem2  16759  prmdiveq  16763  pythagtriplem11  16803  pythagtriplem13  16805  pcgcd1  16855  pcprmpw2  16860  pcaddlem  16866  fldivp1  16875  4sqlem12  16934  4sqlem14  16936  4sqlem15  16937  4sqlem16  16938  vdwapun  16952  mreexexlem4d  17615  acsfn1  17629  acsfn2  17631  sscpwex  17784  rescabs  17802  yonedainv  18249  subm0  18749  pmtrfb  19402  psgnunilem1  19430  odmodnn0  19477  odeq  19487  dfod2  19501  sylow1lem1  19535  lsmsubg  19591  lsmmod  19612  lsmdisj2  19619  ghmplusg  19783  odadd  19787  gexexlem  19789  lt6abl  19832  cyggex2  19834  dprdfinv  19958  dmdprdsplitlem  19976  dpjidcl  19997  ablfacrp  20005  ablfacrp2  20006  ablfac1c  20010  ablfac1eu  20012  acsfn1p  20715  lcomfsupp  20815  lssvancl1  20858  lssvnegcl  20869  lspprvacl  20912  ellspsni  20914  lspsn  20915  lmhmplusg  20958  lmhmima  20961  lmhmpreima  20962  reslmhm  20966  lbsind2  20995  lsmcl  20997  lsmelval2  20999  lsppreli  21004  lspprabs  21009  pj1lmhm  21014  lssvs0or  21027  lspabs3  21038  lspfixed  21045  lspexch  21046  lsmcv  21058  lspsolv  21060  drngnidl  21160  rhmpreimaidl  21194  rngqiprngimfo  21218  rngqiprngfulem4  21231  gzrngunit  21357  zringlpirlem3  21381  prmirredlem  21389  znf1o  21468  znunithash  21481  freshmansdream  21491  frlmsubgval  21681  frlmvplusgvalc  21683  frlmvscaval  21684  frlmphllem  21696  frlmphl  21697  frlmssuvc1  21710  frlmsslsp  21712  frlmup1  21714  frlmup2  21715  lindfind2  21734  lindfrn  21737  f1lindf  21738  islindf4  21754  mplbas2  21956  evlslem3  21994  evlslem1  21996  coe1addfv  22158  lply1binom  22204  evl1addd  22235  evl1subd  22236  evl1muld  22237  mamudi  22297  mamudir  22298  1marepvmarrepid  22469  mdetrlin  22496  smadiadetglem1  22565  smadiadetg  22567  cramerimplem1  22577  mat2pmatscmxcl  22634  m2pmfzgsumcl  22642  pmatcollpw  22675  pmatcollpwfi  22676  pmatcollpw3fi1lem1  22680  cpmidpmatlem2  22765  cpmadugsumlemF  22770  chcoeffeqlem  22779  ntrin  22955  topssnei  23018  restbas  23052  restntr  23076  cnntri  23165  fiuncmp  23298  nllyrest  23380  nllyidm  23383  hausllycmp  23388  cldllycmp  23389  hauspwdom  23395  txcld  23497  txcn  23520  txlly  23530  txnlly  23531  txhaus  23541  txlm  23542  txkgen  23546  xkococnlem  23553  cnmpt2res  23571  xkoinjcn  23581  basqtop  23605  qtopeu  23610  trfbas2  23737  neifil  23774  hausflim  23875  alexsubALTlem2  23942  cnextfval  23956  cnextfvval  23959  cnextf  23960  cnextfres  23963  clssubg  24003  utop2nei  24145  utop3cls  24146  utopreg  24147  psmetlecl  24210  xmetlecl  24241  prdsxmetlem  24263  bldisj  24293  imasf1obl  24383  prdsbl  24386  stdbdmet  24411  stdbdmopn  24413  met2ndci  24417  metcnp  24436  metustto  24448  metustexhalf  24451  cfilucfil  24454  metucn  24466  lssnlm  24596  nmotri  24634  nmoid  24637  tgioo  24691  blcvx  24693  xrsmopn  24708  reperflem  24714  reconnlem2  24723  opnreen  24727  metdsge  24745  metdsre  24749  metdscnlem  24751  metnrmlem1a  24754  metnrmlem1  24755  metnrmlem3  24757  cncfmet  24809  cnmpopc  24829  icopnfcnv  24847  icopnfhmeo  24848  cnllycmp  24862  evth  24865  lebnumii  24872  nmoleub2lem3  25022  iscfil2  25173  cfil3i  25176  iscfil3  25180  cfilfcls  25181  iscau3  25185  iscmet3lem2  25199  caubl  25215  lmcau  25220  cssbn  25282  rrxcph  25299  minveclem2  25333  pjthlem1  25344  pjthlem2  25345  ivthicc  25366  ovollecl  25391  ovolunlem1a  25404  ovolunnul  25408  ovoliunlem1  25410  ismbl2  25435  nulmbl2  25444  unmbl  25445  volun  25453  voliunlem2  25459  ioombl1lem2  25467  uniioombllem2a  25490  uniioombllem3  25493  uniioombllem4  25494  dyaddisjlem  25503  dyadmaxlem  25505  opnmbllem  25509  volsup2  25513  volcn  25514  ismbfd  25547  mbfi1fseqlem1  25623  mbfi1fseqlem5  25627  itg2lecl  25646  itg2monolem2  25659  itg2gt0  25668  itgspliticc  25745  ellimc3  25787  limcres  25794  dvfval  25805  dvres3  25821  dvres3a  25822  dvmptresicc  25824  dvnff  25832  dvnadd  25838  dvn2bss  25839  dvnres  25840  dvcmul  25854  dvcmulf  25855  dvmptres3  25867  dvmptres2  25873  dvmptntr  25882  dvexp3  25889  dvferm1lem  25895  dvlip  25905  dvlipcn  25906  dvlip2  25907  c1liplem1  25908  dvgt0lem1  25914  dvgt0lem2  25915  dvne0  25923  lhop1lem  25925  lhop2  25927  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcvx  25932  dvfsumle  25933  dvfsumleOLD  25934  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  ftc1lem6  25955  ftc1  25956  ftc2ditglem  25959  itgsubstlem  25962  itgpowd  25964  tdeglem4  25972  mdegaddle  25986  mdegmullem  25990  ply1rem  26078  fta1glem2  26081  fta1blem  26083  ig1peu  26087  ig1pdvds  26092  dgrmulc  26184  dgrcolem1  26186  plydivlem4  26211  plydiveu  26213  fta1lem  26222  vieta1lem1  26225  vieta1lem2  26226  plyexmo  26228  taylfvallem1  26271  taylfval  26273  tayl0  26276  taylplem1  26277  taylply2  26282  taylply2OLD  26283  taylply  26284  dvtaylp  26285  dvntaylp  26286  dvntaylp0  26287  taylthlem1  26288  taylthlem2  26289  taylthlem2OLD  26290  ulmcaulem  26310  ulmcau  26311  ulmcn  26315  ulmdvlem1  26316  radcnvlem1  26329  radcnvle  26336  psercn  26343  pserdvlem2  26345  pserdv  26346  abelth  26358  tanregt0  26455  dvlog2lem  26568  efopn  26574  logtayllem  26575  logccv  26579  cxplt3  26616  cxpmul2zd  26632  cxpltd  26635  cxpled  26636  cxplt3d  26651  cxple3d  26652  dvsqrt  26658  cxpcn3  26665  cxpaddle  26669  cxpeq  26674  angcan  26719  angvald  26721  ang180lem2  26727  ang180  26731  isosctrlem3  26737  dquartlem1  26768  atantayl2  26855  leibpi  26859  log2tlbnd  26862  birthdaylem3  26870  xrlimcnp  26885  efrlim  26886  efrlimOLD  26887  o1cxp  26892  jensenlem2  26905  jensen  26906  fsumharmonic  26929  lgamucov  26955  lgamcvg2  26972  wilthlem1  26985  basellem3  27000  basellem6  27003  basellem8  27005  ppisval  27021  chtwordi  27073  ppiwordi  27079  mumullem2  27097  mpodvdsmulf1o  27111  dvdsmulf1o  27113  fsumvma  27131  fsumvma2  27132  chpchtsum  27137  chpub  27138  logfacubnd  27139  dchrmulcl  27167  dchrinv  27179  dchrptlem1  27182  dchrptlem2  27183  sumdchr2  27188  dchr2sum  27191  bposlem7  27208  lgslem1  27215  lgslem3  27217  lgsdirprm  27249  lgsqrlem2  27265  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem4  27296  lgseisen  27297  lgsquadlem1  27298  lgsquad2lem1  27302  lgsquad3  27305  m1lgs  27306  2sqlem7  27342  2sq2  27351  2sqmod  27354  chebbnd1lem2  27388  chebbnd1lem3  27389  rplogsumlem1  27402  rpvmasumlem  27405  dchrvmasumlem1  27413  dchrvmasum2lem  27414  dchrvmasumlema  27418  dchrisum0flblem2  27427  dchrisum0fno1  27429  dchrisum0re  27431  logdivsum  27451  pntrsumbnd2  27485  pntpbnd1a  27503  pntpbnd1  27504  pntibndlem2  27509  pntlemr  27520  pntlemj  27521  pntlemf  27523  pnt2  27531  padicabv  27548  ostth2lem2  27552  sltrec  27739  madebday  27818  sltn0  27824  addsproplem6  27888  sleadd1  27903  negsproplem6  27946  mulsproplem13  28038  mulsproplem14  28039  sltmuld  28047  mulsgt0d  28055  onscutlt  28172  n0sfincut  28253  halfcut  28340  f1otrg  28805  brbtwn2  28839  colinearalglem2  28841  axcgrtr  28849  axcgrid  28850  axsegconlem7  28857  axsegcon  28861  ax5seglem3  28865  ax5seglem6  28868  ax5seg  28872  axpaschlem  28874  axlowdimlem17  28892  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  ecgrtg  28917  usgredg2v  29161  vtxdgoddnumeven  29488  2trlond  29876  eupthp1  30152  nmobndi  30711  ubthlem2  30807  ubthlem3  30808  minvecolem2  30811  shuni  31236  pjhthlem1  31327  chscllem2  31574  pjcompi  31608  mayete3i  31664  unoplin  31856  hmoplin  31878  nmophmi  31967  mdslmd4i  32269  isoun  32632  submuladdd  32670  receqid  32675  xrge0addcld  32692  xrofsup  32697  eliccelico  32707  elicoelioo  32708  difioo  32712  hashpss  32741  sgnmul  32767  rexdiv  32853  mgcmnt1d  32930  mgcmnt2d  32931  chnub  32945  xrge0addgt0  32965  omndadd2d  33029  omndadd2rd  33030  omndmul2  33033  cycpmcl  33080  cycpm2tr  33083  cyc3evpm  33114  cycpmconjslem2  33119  fldgensdrg  33271  ofldchr  33299  qusker  33327  eqgvscpbl  33328  ringlsmss1  33374  ringlsmss2  33375  lidlmcld  33397  intlidl  33398  lidlunitel  33401  elrspunidl  33406  idlinsubrg  33409  isprmidlc  33425  rhmpreimaprmidl  33429  qsidomlem1  33430  ssdifidllem  33434  mxidlmaxv  33446  mxidlprm  33448  ssmxidllem  33451  opprmxidlabs  33465  qsdrnglem2  33474  resssra  33590  ply1degltdimlem  33625  lindsunlem  33627  sdrgfldext  33653  fldsdrgfldext  33664  finexttrb  33667  fldgenfldext  33670  fldextrspunlem1  33677  algextdeglem4  33717  algextdeglem8  33721  constrextdg2lem  33745  mdetpmtr2  33821  mdetpmtr12  33822  madjusmdetlem1  33824  madjusmdetlem4  33827  rhmpreimacn  33882  unitdivcld  33898  xrge0mulc1cn  33938  qqhnm  33987  esumcst  34060  esumfsup  34067  esumpmono  34076  esumcvg  34083  difelsiga  34130  sigapisys  34152  sigapildsys  34159  ldgenpisyslem1  34160  1stmbfm  34258  2ndmbfm  34259  dya2icoseg  34275  sibfinima  34337  probmeasb  34428  orvcgteel  34466  orvclteel  34471  ballotlemsima  34514  ballotlemfrceq  34527  ccatmulgnn0dir  34540  fct2relem  34595  ftc2re  34596  chtvalz  34627  subfacp1lem2a  35174  subfaclim  35182  erdsze2lem2  35198  cvmliftlem2  35280  cvmliftlem10  35288  cvmliftlem13  35290  cvmliftiota  35295  cvmlift2lem9  35305  cvmlift2lem11  35307  cvmlift2lem12  35308  cvmliftphtlem  35311  cvmlift3lem6  35318  cvmlift3lem7  35319  cvmlift3lem9  35321  snmlff  35323  mrsubfval  35502  wzel  35819  wsuclem  35820  brsegle  36103  opnregcld  36325  weiunfrlem  36459  fin2so  37608  poimirlem17  37638  poimirlem23  37644  opnmbllem0  37657  mblfinlem3  37660  mblfinlem4  37661  itg2addnclem  37672  itg2addnc  37675  itg2gt0cn  37676  ftc1cnnclem  37692  ftc1cnnc  37693  areacirclem5  37713  indexdom  37735  sstotbnd2  37775  isbnd3  37785  isbnd3b  37786  cntotbnd  37797  ismtyima  37804  heibor1lem  37810  heiborlem8  37819  rrncmslem  37833  reheibor  37840  lkrlsp  39102  lshpkrlem5  39114  ldualssvscl  39158  ldualssvsubcl  39159  llnmlplnN  39540  llncvrlpln  39559  pmapjat1  39854  pclfinN  39901  lautlt  40092  lauteq  40096  lautco  40098  ltrn11  40127  ltrnle  40130  ltrneq2  40149  cdlemednuN  40301  cdleme20k  40320  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme21c  40328  cdleme22e  40345  cdleme22eALTN  40346  cdlemefrs32fva  40401  cdlemg4g  40617  cdlemg18b  40680  cdlemg18c  40681  cdlemj3  40824  dia2dimlem5  41069  dvhopN  41117  cdlemm10N  41119  dihjatcclem4  41422  dochexmidlem2  41462  lclkrlem2o  41522  lcfrlem5  41547  lcfrlem6  41548  lcdlssvscl  41607  mapdpglem6  41679  mapdpglem9  41681  mapdpglem12  41684  mapdpglem14  41686  mapdindp0  41720  hdmaprnlem7N  41856  hdmaprnlem8N  41857  hdmaprnlem3eN  41859  hgmapvvlem3  41926  dvun  42354  addinvcom  42427  evlsaddval  42563  evlsmulval  42564  evladdval  42570  evlmulval  42571  mzpsubst  42743  eldioph2lem1  42755  eldioph2lem2  42756  eldioph2b  42758  diophin  42767  irrapxlem2  42818  irrapxlem4  42820  irrapxlem5  42821  pellexlem1  42824  pellexlem2  42825  pellexlem6  42829  elpell1qr2  42867  pell1qrgaplem  42868  pell1qrgap  42869  pellqrex  42874  pellfundex  42881  pellfund14  42893  rmspecsqrtnq  42901  rmxyadd  42917  congsub  42966  mzpcong  42968  congrep  42969  acongtr  42974  acongrep  42976  jm2.19lem1  42985  jm2.22  42991  jm2.23  42992  jm2.26lem3  42997  jm2.26  42998  jm2.27a  43001  fnwe2lem2  43047  aomclem6  43055  hbtlem2  43120  hbtlem4  43122  hbtlem5  43124  dgraa0p  43145  rngunsnply  43165  proot1hash  43191  nnoeomeqom  43308  cantnf2  43321  omabs2  43328  naddcnff  43358  naddcnffo  43360  naddcnfcom  43362  naddcnfid1  43363  expgrowth  44331  fpmd  45264  abslt2sqd  45363  ioondisj2  45498  ioondisj1  45499  eliocre  45514  ioossioobi  45522  iooiinicc  45547  iooiinioc  45561  lptioo2  45636  limcresiooub  45647  limsupequzlem  45727  xlimmnfvlem2  45838  xlimpnfvlem2  45842  cncfuni  45891  cncfiooicclem1  45898  cxpcncf2  45904  dvcnre  45921  dvresntr  45923  dvresioo  45926  dvbdfbdioolem1  45933  dvnmptdivc  45943  dvnxpaek  45947  itgsinexplem1  45959  itgcoscmulx  45974  itgiccshift  45985  itgperiod  45986  ovolsplit  45993  stoweidlem11  46016  stoweidlem26  46031  stoweidlem34  46039  stoweidlem36  46041  stoweidlem38  46043  stirlinglem5  46083  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem20  46132  fourierdlem58  46169  fourierdlem72  46183  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem79  46190  fourierdlem80  46191  fourierdlem87  46198  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  fourierdlem113  46224  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  etransclem46  46285  etransclem47  46286  rrndistlt  46295  rrnprjdstle  46306  ioorrnopnxrlem  46311  sge0ssre  46402  sge0seq  46451  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmvlelem1  46600  hoidifhspdmvle  46625  hoiqssbllem2  46628  ovolval5lem2  46658  iinhoiicc  46679  iunhoiioo  46681  vonioolem2  46686  vonicclem2  46689  issmflem  46732  submodlt  47355  iccpartdisj  47442  m1expevenALTV  47652  fpprel2  47746  tgoldbach  47822  opstrgric  47930  gpg3kgrtriex  48084  nn0eo  48521  fdivpm  48536  refdivpm  48537  elbigolo1  48550  logbpw2m1  48560  fllog2  48561  dignn0flhalflem1  48608  dignn0flhalflem2  48609  itsclinecirc0in  48768  2itscplem2  48772  itscnhlinecirc02plem1  48775  iccdisj2  48889