Theorem syl22anc 852

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 521	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 850	1 ⊢ (𝜑 → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  preqsnd  4819  fr2nr  5632  soltmin  6130  f1oprg  6864  f1prex  7285  fveqf1o  7303  weniso  7357  fr3nr  7771  suppofssd  8201  smogt  8356  smocdmdom  8357  oacomf1o  8552  en2prd  9054  difsnen  9057  enfixsn  9084  domss2  9134  ssenen  9149  marypha1lem  9403  fisupcl  9440  ordtypelem3  9492  ordtypelem8  9497  oieu  9511  oismo  9512  wofib  9517  wemaplem2  9519  wemapso  9523  wemapso2lem  9524  unxpwdom2  9560  infdifsn  9636  oemapvali  9663  cantnflem1c  9666  cantnflem1  9668  cantnf  9672  cnfcom3  9683  r1ordg  9760  dif1card  10013  infxpenlem  10016  dfac8clem  10035  infxp  10216  infmap2  10219  cflim2  10265  coftr  10275  fin2i2  10320  enfin2i  10323  fin23lem26  10327  fin23lem27  10330  fin23lem40  10353  isf32lem2  10356  isf32lem3  10357  isf32lem4  10358  isf32lem7  10361  isf32lem9  10363  fin1a2lem13  10414  fin12  10415  alephexp1  10588  gchdomtri  10638  fpwwe2lem11  10650  fpwwe2lem12  10651  gchpwdom  10679  gchhar  10688  adderpqlem  10963  mulerpqlem  10964  addassnq  10967  mulassnq  10968  distrnq  10970  mulidnq  10972  recmulnq  10973  ltexnq  10984  distrlem1pr  11034  distrlem4pr  11035  prlem936  11056  reclem3pr  11058  mulcmpblnr  11080  mulgt0d  11389  mul4d  11446  add4d  11463  add42d  11464  subcan  11537  addsub4d  11640  subadd4d  11641  sub4d  11642  2addsubd  11643  addsubeq4d  11644  muladdd  11696  mulsubd  11697  addgegt0d  11811  addgtge0d  11812  addge0d  11814  mulge0d  11815  le2subd  11858  ltleaddd  11859  leltaddd  11860  lt2subd  11862  divdivdiv  11940  divcan5  11941  divne0d  12031  recdivd  12032  recdiv2d  12033  divcan6d  12034  ddcand  12035  rec11d  12036  divmuldivd  12056  divmul13d  12057  divmul24d  12058  divadddivd  12059  divsubdivd  12060  divmuleqd  12061  divdivdivd  12062  mulge0b  12109  recreclt  12138  divgt0d  12174  mulgt1d  12175  lemulge11d  12176  lemulge12d  12177  ltmul12ad  12180  lemul12ad  12181  lemul12bd  12182  supmul1  12208  nndivtr  12307  qreccl  13019  ledivdivd  13111  lediv12ad  13145  lt2mul2divd  13155  xlt2add  13312  supxrun  13368  supxrre  13379  infxrre  13389  elicore  13451  iccss2  13470  iccssico2  13473  icossico2d  13474  lincmb01cmp  13548  iccf1o  13549  nnge2recico01  13560  fzrev2i  13644  2tnp1ge0ge0  13890  m1modnnsub1  13981  modaddmodup  13998  modaddmodlo  13999  modsubdir  14004  fzennn  14032  sermono  14098  mulexpz  14166  expaddz  14170  sqdiv  14185  expsubd  14221  ltexp2a  14230  expmordi  14231  leexp2a  14236  expmulnbnd  14299  digit1  14301  lt2sqd  14320  le2sqd  14321  sq11d  14322  bcm1k  14379  bcp1n  14380  bcp1nk  14381  hashpss  14474  hashf1lem1  14520  cshw1  14893  2swrd2eqwrdeq  15026  ofccat  15042  sgnmul  15180  absrele  15395  sqreulem  15447  sqrtmuld  15512  sqrtsq2d  15513  sqrtled  15514  sqrtltd  15515  sqr11d  15516  abs3lemd  15551  rlimuni  15637  climuni  15639  lo1resb  15651  o1resb  15653  2clim  15659  addcn2  15681  mulcn2  15683  o1of2  15700  o1rlimmul  15706  lo1add  15714  lo1mul  15715  isercolllem1  15752  caucvgrlem  15760  iseraltlem2  15770  iseraltlem3  15771  mptfzshft  15864  fsumrev  15865  fsum0diag2  15869  binomlem  15918  climcndslem1  15938  climcndslem2  15939  harmonic  15948  mertenslem1  15973  fprodser  16036  fprodrev  16064  efcllem  16163  moddvds  16353  dvds1  16409  dvdsext  16411  evennn2n  16441  bitsinv1  16532  sadaddlem  16556  sadasslem  16560  sadeq  16562  mulgcd  16638  dvdssqlem  16656  lcmftp  16726  rpmulgcd2  16746  coprmproddvdslem  16752  isprm5  16798  isprm6  16805  crth  16869  eulerthlem2  16873  prmdiveq  16877  pythagtriplem11  16917  pythagtriplem13  16919  pcgcd1  16969  pcprmpw2  16974  pcaddlem  16980  fldivp1  16989  4sqlem12  17048  4sqlem14  17050  4sqlem15  17051  4sqlem16  17052  vdwapun  17066  mreexexlem4d  17735  acsfn1  17749  acsfn2  17751  sscpwex  17904  rescabs  17922  yonedainv  18369  chnub  18710  subm0  18924  pmtrfb  19592  psgnunilem1  19620  odmodnn0  19667  odeq  19677  dfod2  19691  sylow1lem1  19725  lsmsubg  19781  lsmmod  19802  lsmdisj2  19809  ghmplusg  19973  odadd  19977  gexexlem  19979  lt6abl  20022  cyggex2  20024  dprdfinv  20148  dmdprdsplitlem  20166  dpjidcl  20187  ablfacrp  20195  ablfacrp2  20196  ablfac1c  20200  ablfac1eu  20202  omndadd2d  20257  omndadd2rd  20258  omndmul2  20260  acsfn1p  20965  lcomfsupp  21086  lssvancl1  21129  lssvnegcl  21140  lspprvacl  21183  ellspsni  21185  lspsn  21186  lmhmplusg  21228  lmhmima  21231  lmhmpreima  21232  reslmhm  21236  lbsind2  21265  lsmcl  21267  lsmelval2  21269  lsppreli  21274  lspprabs  21279  pj1lmhm  21284  lssvs0or  21297  lspabs3  21308  lspfixed  21315  lspexch  21316  lsmcv  21328  lspsolv  21330  lidlmcld  21415  drngnidl  21440  rhmpreimaidl  21479  rngqiprngimfo  21504  rngqiprngfulem4  21517  isprmidlc  21535  rhmpreimaprmidl  21542  qsidomlem1  21543  ssdifidllem  21547  gzrngunit  21646  zringlpirlem3  21677  prmirredlem  21685  znf1o  21764  znunithash  21777  freshmansdream  21787  ofldchr  21789  frlmsubgval  21978  frlmvplusgvalc  21980  frlmvscaval  21981  frlmphllem  21993  frlmphl  21994  frlmssuvc1  22007  frlmsslsp  22009  frlmup1  22011  frlmup2  22012  lindfind2  22031  lindfrn  22034  f1lindf  22035  islindf4  22051  mplbas2  22258  evlslem3  22296  evlslem1  22298  evladdval  22319  evlmulval  22320  evlsaddval  22345  evlsmulval  22346  coe1addfv  22491  lply1binom  22535  evl1addd  22566  evl1subd  22567  evl1muld  22568  mamudi  22625  mamudir  22626  1marepvmarrepid  22797  mdetrlin  22824  smadiadetglem1  22893  smadiadetg  22895  cramerimplem1  22908  mat2pmatscmxcl  22965  m2pmfzgsumcl  22973  pmatcollpw  23006  pmatcollpwfi  23007  pmatcollpw3fi1lem1  23011  cpmidpmatlem2  23096  cpmadugsumlemF  23101  chcoeffeqlem  23110  ntrin  23286  topssnei  23349  restbas  23383  restntr  23407  cnntri  23496  fiuncmp  23629  nllyrest  23712  nllyidm  23715  hausllycmp  23720  cldllycmp  23721  hauspwdom  23727  txcld  23829  txcn  23852  txlly  23862  txnlly  23863  txhaus  23873  txlm  23874  txkgen  23878  xkococnlem  23885  cnmpt2res  23903  xkoinjcn  23913  basqtop  23937  qtopeu  23942  trfbas2  24069  neifil  24106  hausflim  24207  alexsubALTlem2  24274  cnextfval  24288  cnextfvval  24291  cnextf  24292  cnextfres  24295  clssubg  24335  utop2nei  24476  utop3cls  24477  utopreg  24478  psmetlecl  24541  xmetlecl  24572  prdsxmetlem  24594  bldisj  24624  imasf1obl  24714  prdsbl  24717  stdbdmet  24742  stdbdmopn  24744  met2ndci  24748  metcnp  24767  metustto  24779  metustexhalf  24782  cfilucfil  24785  metucn  24797  lssnlm  24927  nmotri  24965  nmoid  24968  tgioo  25022  blcvx  25024  xrsmopn  25039  reperflem  25045  reconnlem2  25054  opnreen  25058  metdsge  25076  metdsre  25080  metdscnlem  25082  metnrmlem1a  25085  metnrmlem1  25086  metnrmlem3  25088  cncfmet  25137  cnmpopc  25156  icopnfcnv  25170  icopnfhmeo  25171  cnllycmp  25184  evth  25187  lebnumii  25194  nmoleub2lem3  25343  iscfil2  25494  cfil3i  25497  iscfil3  25501  cfilfcls  25502  iscau3  25506  iscmet3lem2  25520  caubl  25536  lmcau  25541  cssbn  25603  rrxcph  25620  minveclem2  25654  pjthlem1  25665  pjthlem2  25666  ivthicc  25686  ovollecl  25711  ovolunlem1a  25724  ovolunnul  25728  ovoliunlem1  25730  ismbl2  25755  nulmbl2  25764  unmbl  25765  volun  25773  voliunlem2  25779  ioombl1lem2  25787  uniioombllem2a  25810  uniioombllem3  25813  uniioombllem4  25814  dyaddisjlem  25823  dyadmaxlem  25825  opnmbllem  25829  volsup2  25833  volcn  25834  ismbfd  25867  mbfi1fseqlem1  25943  mbfi1fseqlem5  25947  itg2lecl  25966  itg2monolem2  25979  itg2gt0  25988  itgspliticc  26064  ellimc3  26106  limcres  26113  dvfval  26124  dvres3  26140  dvres3a  26141  dvmptresicc  26143  dvnff  26150  dvnadd  26156  dvn2bss  26157  dvnres  26158  dvcmul  26171  dvcmulf  26172  dvmptres3  26183  dvmptres2  26189  dvmptntr  26198  dvexp3  26205  dvferm1lem  26211  dvlip  26220  dvlipcn  26221  dvlip2  26222  c1liplem1  26223  dvgt0lem1  26229  dvgt0lem2  26230  dvne0  26238  lhop1lem  26240  lhop2  26242  lhop  26243  dvcnvrelem1  26244  dvcnvrelem2  26245  dvcvx  26247  dvfsumle  26248  dvfsumabs  26250  dvfsumlem2  26254  ftc1lem6  26268  ftc1  26269  ftc2ditglem  26272  itgsubstlem  26275  itgpowd  26277  tdeglem4  26285  mdegaddle  26299  mdegmullem  26303  ply1rem  26391  fta1glem2  26394  fta1blem  26396  ig1peu  26400  ig1pdvds  26405  dgrmulc  26497  dgrcolem1  26499  plydivlem4  26526  plydiveu  26528  fta1lem  26537  vieta1lem1  26542  vieta1lem2  26543  plyexmo  26545  taylfvallem1  26593  taylfval  26595  tayl0  26598  taylplem1  26599  taylply2  26604  taylply  26605  dvtaylp  26606  dvntaylp  26607  dvntaylp0  26608  taylthlem1  26609  taylthlem2  26610  ulmcaulem  26630  ulmcau  26631  ulmcn  26635  ulmdvlem1  26636  radcnvlem1  26649  radcnvle  26656  psercn  26662  pserdvlem2  26664  pserdv  26665  abelth  26677  tanregt0  26776  dvlog2lem  26889  efopn  26895  logtayllem  26896  logccv  26900  cxplt3  26937  cxpmul2zd  26953  cxpltd  26956  cxpled  26957  cxplt3d  26972  cxple3d  26973  dvsqrt  26979  cxpcn3  26985  cxpaddle  26989  cxpeq  26994  angcan  27039  angvald  27041  ang180lem2  27047  ang180  27051  isosctrlem3  27057  dquartlem1  27088  atantayl2  27175  leibpi  27179  log2tlbnd  27182  birthdaylem3  27190  xrlimcnp  27205  efrlim  27206  o1cxp  27211  jensenlem2  27224  jensen  27225  fsumharmonic  27248  lgamucov  27274  lgamcvg2  27291  wilthlem1  27304  basellem3  27319  basellem6  27322  basellem8  27324  ppisval  27340  chtwordi  27392  ppiwordi  27398  mumullem2  27416  mpodvdsmulf1o  27430  dvdsmulf1o  27432  fsumvma  27449  fsumvma2  27450  chpchtsum  27455  chpub  27456  logfacubnd  27457  dchrmulcl  27485  dchrinv  27497  dchrptlem1  27500  dchrptlem2  27501  sumdchr2  27506  dchr2sum  27509  bposlem7  27526  lgslem1  27533  lgslem3  27535  lgsdirprm  27567  lgsqrlem2  27583  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem4  27614  lgseisen  27615  lgsquadlem1  27616  lgsquad2lem1  27620  lgsquad3  27623  m1lgs  27624  2sqlem7  27660  2sq2  27669  2sqmod  27672  chebbnd1lem2  27706  chebbnd1lem3  27707  rplogsumlem1  27720  rpvmasumlem  27723  dchrvmasumlem1  27731  dchrvmasum2lem  27732  dchrvmasumlema  27736  dchrisum0flblem2  27745  dchrisum0fno1  27747  dchrisum0re  27749  logdivsum  27769  pntrsumbnd2  27803  pntpbnd1a  27821  pntpbnd1  27822  pntibndlem2  27827  pntlemr  27838  pntlemj  27839  pntlemf  27841  pnt2  27849  padicabv  27866  ostth2lem2  27870  lesrecd  28065  ltsrecd  28067  madebday  28165  addsproplem6  28239  negsproplem6  28298  mulsproplem13  28393  mulsproplem14  28394  ltmulsd  28402  mulsgt0d  28410  angmgmaddov2  29268  f1otrg  29327  brbtwn2  29362  colinearalglem2  29364  axcgrtr  29372  axcgrid  29373  axsegconlem7  29380  axsegcon  29384  ax5seglem3  29388  ax5seglem6  29391  ax5seg  29395  axpaschlem  29397  axlowdimlem17  29415  axcontlem2  29422  axcontlem4  29424  axcontlem7  29427  axcontlem8  29428  ecgrtg  29440  usgredg2v  29687  vtxdgoddnumeven  30013  2trlond  30407  eupthp1  30696  nmobndi  31256  ubthlem2  31352  ubthlem3  31353  minvecolem2  31356  shuni  31781  pjhthlem1  31872  chscllem2  32119  pjcompi  32153  mayete3i  32209  unoplin  32401  hmoplin  32423  nmophmi  32512  mdslmd4i  32814  isoun  33174  submuladdd  33211  receqid  33215  xrge0addcld  33233  xrofsup  33238  eliccelico  33248  elicoelioo  33249  difioo  33253  rexdiv  33371  mgcmnt1d  33437  mgcmnt2d  33438  xrge0addgt0  33457  cycpmcl  33556  cycpm2tr  33559  cyc3evpm  33590  cycpmconjslem2  33595  fldgensdrg  33755  qusker  33789  eqgvscpbl  33790  ringlsmss1  33827  ringlsmss2  33828  intlidl  33848  lidlunitel  33851  elrspunidl  33856  idlinsubrg  33859  mxidlmaxv  33871  mxidlprm  33873  ssmxidllem  33876  opprmxidlabs  33889  qsdrnglem2  33898  dflring3  33907  dflring4  33908  selvply1rhmlem4  34033  mplvrpmmhm  34056  mplvrpmrhm  34057  esplyind  34085  resssra  34097  ply1degltdimlem  34132  lindsunlem  34134  sdrgfldext  34160  fldsdrgfldext  34171  finexttrb  34175  fldgenfldext  34178  fldextrspunlem1  34185  algextdeglem4  34230  algextdeglem8  34234  constrextdg2lem  34258  mdetpmtr2  34334  mdetpmtr12  34335  madjusmdetlem1  34337  madjusmdetlem4  34340  rhmpreimacn  34395  unitdivcld  34411  xrge0mulc1cn  34451  qqhnm  34500  esumcst  34573  esumfsup  34580  esumpmono  34589  esumcvg  34596  sigapisys  34666  sigapildsys  34673  ldgenpisyslem1  34674  1stmbfm  34771  2ndmbfm  34772  dya2icoseg  34788  sibfinima  34850  probmeasb  34941  orvcgteel  34979  orvclteel  34984  ballotlemsima  35027  ballotlemfrceq  35040  ccatmulgnn0dir  35053  fct2relem  35105  ftc2re  35106  chtvalz  35137  r1filimi  35611  subfacp1lem2a  35759  subfaclim  35767  erdsze2lem2  35783  cvmliftlem2  35865  cvmliftlem10  35873  cvmliftlem13  35875  cvmliftiota  35880  cvmlift2lem9  35890  cvmlift2lem11  35892  cvmlift2lem12  35893  cvmliftphtlem  35896  cvmlift3lem6  35903  cvmlift3lem7  35904  cvmlift3lem9  35906  snmlff  35908  mrsubfval  36087  wzel  36401  wsuclem  36402  brsegle  36688  nmulel1  36795  nadddilem1  36800  nadddilem3  36802  opnregcld  36949  weiunfrlem  37083  fin2so  38361  poimirlem17  38386  poimirlem23  38392  opnmbllem0  38405  mblfinlem3  38408  mblfinlem4  38409  itg2addnclem  38420  itg2addnc  38423  itg2gt0cn  38424  ftc1cnnclem  38440  ftc1cnnc  38441  areacirclem5  38461  indexdom  38484  sstotbnd2  38524  isbnd3  38534  isbnd3b  38535  cntotbnd  38546  ismtyima  38553  heibor1lem  38559  heiborlem8  38568  rrncmslem  38582  reheibor  38589  lkrlsp  39975  lshpkrlem5  39987  ldualssvscl  40031  ldualssvsubcl  40032  llnmlplnN  40412  llncvrlpln  40431  pmapjat1  40726  pclfinN  40773  lautlt  40964  lauteq  40968  lautco  40970  ltrn11  40999  ltrnle  41002  ltrneq2  41021  cdlemednuN  41173  cdleme20k  41192  cdleme20l2  41194  cdleme20l  41195  cdleme20m  41196  cdleme21c  41200  cdleme22e  41217  cdleme22eALTN  41218  cdlemefrs32fva  41273  cdlemg4g  41489  cdlemg18b  41552  cdlemg18c  41553  cdlemj3  41696  dia2dimlem5  41941  dvhopN  41989  cdlemm10N  41991  dihjatcclem4  42294  dochexmidlem2  42334  lclkrlem2o  42394  lcfrlem5  42419  lcfrlem6  42420  lcdlssvscl  42479  mapdpglem6  42551  mapdpglem9  42553  mapdpglem12  42556  mapdpglem14  42558  mapdindp0  42592  hdmaprnlem7N  42728  hdmaprnlem8N  42729  hdmaprnlem3eN  42731  hgmapvvlem3  42798  dvun  43234  addinvcom  43307  mzpsubst  43593  eldioph2lem1  43605  eldioph2lem2  43606  eldioph2b  43608  diophin  43617  irrapxlem2  43664  irrapxlem4  43666  irrapxlem5  43667  pellexlem1  43670  pellexlem2  43671  pellexlem6  43675  elpell1qr2  43713  pell1qrgaplem  43714  pell1qrgap  43715  pellqrex  43720  pellfundex  43727  pellfund14  43739  rmspecsqrtnq  43747  rmxyadd  43762  congsub  43811  mzpcong  43813  congrep  43814  acongtr  43819  acongrep  43821  jm2.19lem1  43830  jm2.22  43836  jm2.23  43837  jm2.26lem3  43842  jm2.26  43843  jm2.27a  43846  fnwe2lem2  43892  aomclem6  43900  hbtlem2  43965  hbtlem4  43967  hbtlem5  43969  dgraa0p  43990  rngunsnply  44010  proot1hash  44036  nnoeomeqom  44153  cantnf2  44166  omabs2  44173  naddcnff  44203  naddcnffo  44205  naddcnfcom  44207  naddcnfid1  44208  expgrowth  45159  fpmd  46092  abslt2sqd  46190  ioondisj2  46323  ioondisj1  46324  eliocre  46339  ioossioobi  46347  iooiinicc  46372  iooiinioc  46386  lptioo2  46461  limcresiooub  46470  limsupequzlem  46550  xlimmnfvlem2  46661  xlimpnfvlem2  46665  cncfuni  46714  cncfiooicclem1  46721  cxpcncf2  46727  dvcnre  46744  dvresntr  46746  dvresioo  46749  dvbdfbdioolem1  46756  dvnmptdivc  46766  dvnxpaek  46770  itgsinexplem1  46782  itgcoscmulx  46797  itgiccshift  46808  itgperiod  46809  ovolsplit  46816  stoweidlem11  46839  stoweidlem26  46854  stoweidlem34  46862  stoweidlem36  46864  stoweidlem38  46866  stirlinglem5  46906  dirkercncflem2  46932  dirkercncflem4  46934  fourierdlem20  46955  fourierdlem58  46992  fourierdlem72  47006  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem79  47013  fourierdlem80  47014  fourierdlem87  47021  fourierdlem94  47028  fourierdlem103  47037  fourierdlem104  47038  fourierdlem107  47041  fourierdlem113  47047  sqwvfoura  47056  sqwvfourb  47057  fourierswlem  47058  fouriersw  47059  etransclem46  47108  etransclem47  47109  rrndistlt  47118  rrnprjdstle  47129  ioorrnopnxrlem  47134  sge0ssre  47225  sge0seq  47274  hsphoidmvle2  47413  hsphoidmvle  47414  hoidmv1lelem1  47419  hoidmv1lelem2  47420  hoidmv1lelem3  47421  hoidmvlelem1  47423  hoidifhspdmvle  47448  hoiqssbllem2  47451  ovolval5lem2  47481  iinhoiicc  47502  iunhoiioo  47504  vonioolem2  47509  vonicclem2  47512  issmflem  47555  sqrtnnaa  47731  submodlt  48244  iccpartdisj  48337  m1expevenALTV  48563  fpprel2  48657  tgoldbach  48733  opstrgric  48842  gpg3kgrtriex  49005  nn0eo  49458  fdivpm  49473  refdivpm  49474  elbigolo1  49487  logbpw2m1  49497  fllog2  49498  dignn0flhalflem1  49545  dignn0flhalflem2  49546  itsclinecirc0in  49705  2itscplem2  49709  itscnhlinecirc02plem1  49712  iccdisj2  49823