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  5628  soltmin  6130  f1oprg  6869  f1prex  7290  fveqf1o  7308  weniso  7362  fr3nr  7784  suppofssd  8213  smogt  8368  smocdmdom  8369  oacomf1o  8566  en2prd  9068  difsnen  9071  enfixsn  9098  domss2  9148  ssenen  9163  marypha1lem  9418  fisupcl  9455  ordtypelem3  9507  ordtypelem8  9512  oieu  9526  oismo  9527  wofib  9532  wemaplem2  9534  wemapso  9538  wemapso2lem  9539  unxpwdom2  9575  infdifsn  9651  oemapvali  9678  cantnflem1c  9681  cantnflem1  9683  cantnf  9687  cnfcom3  9698  r1ordg  9778  r1filimi  9896  dif1card  10082  infxpenlem  10085  dfac8clem  10104  infxp  10285  infmap2  10288  cflim2  10334  coftr  10344  fin2i2  10389  enfin2i  10392  fin23lem26  10396  fin23lem27  10399  fin23lem40  10422  isf32lem2  10425  isf32lem3  10426  isf32lem4  10427  isf32lem7  10430  isf32lem9  10432  fin1a2lem13  10483  fin12  10484  alephexp1  10657  gchdomtri  10707  fpwwe2lem11  10719  fpwwe2lem12  10720  gchpwdom  10748  gchhar  10757  adderpqlem  11032  mulerpqlem  11033  addassnq  11036  mulassnq  11037  distrnq  11039  mulidnq  11041  recmulnq  11042  ltexnq  11053  distrlem1pr  11103  distrlem4pr  11104  prlem936  11125  reclem3pr  11127  mulcmpblnr  11149  mulgt0d  11458  mul4d  11515  add4d  11532  add42d  11533  subcan  11606  addsub4d  11709  subadd4d  11710  sub4d  11711  2addsubd  11712  addsubeq4d  11713  muladdd  11767  mulsubd  11768  addgegt0d  11882  addgtge0d  11883  addge0d  11885  mulge0d  11886  le2subd  11929  ltleaddd  11930  leltaddd  11931  lt2subd  11933  divdivdiv  12011  divcan5  12012  divne0d  12102  recdivd  12103  recdiv2d  12104  divcan6d  12105  ddcand  12106  rec11d  12107  divmuldivd  12127  divmul13d  12128  divmul24d  12129  divadddivd  12130  divsubdivd  12131  divmuleqd  12132  divdivdivd  12133  mulge0b  12180  recreclt  12209  divgt0d  12245  mulgt1d  12246  lemulge11d  12247  lemulge12d  12248  ltmul12ad  12251  lemul12ad  12252  lemul12bd  12253  supmul1  12279  nndivtr  12378  qreccl  13090  ledivdivd  13182  lediv12ad  13216  lt2mul2divd  13226  xlt2add  13383  supxrun  13439  supxrre  13450  infxrre  13460  elicore  13522  iccss2  13541  iccssico2  13544  icossico2d  13545  lincmb01cmp  13619  iccf1o  13620  nnge2recico01  13631  fzrev2i  13716  2tnp1ge0ge0  13962  m1modnnsub1  14053  modaddmodup  14070  modaddmodlo  14071  modsubdir  14076  fzennn  14104  sermono  14170  mulexpz  14238  expaddz  14242  sqdiv  14257  expsubd  14293  ltexp2a  14302  expmordi  14303  leexp2a  14308  expmulnbnd  14372  digit1  14374  lt2sqd  14393  le2sqd  14394  sq11d  14395  bcm1k  14452  bcp1n  14453  bcp1nk  14454  hashpss  14547  hashf1lem1  14593  cshw1  14966  2swrd2eqwrdeq  15099  ofccat  15115  sgnmul  15253  absrele  15468  sqreulem  15520  sqrtmuld  15585  sqrtsq2d  15586  sqrtled  15587  sqrtltd  15588  sqr11d  15589  abs3lemd  15624  rlimuni  15710  climuni  15712  lo1resb  15724  o1resb  15726  2clim  15732  addcn2  15754  mulcn2  15756  o1of2  15773  o1rlimmul  15779  lo1add  15787  lo1mul  15788  isercolllem1  15825  caucvgrlem  15833  iseraltlem2  15843  iseraltlem3  15844  mptfzshft  15937  fsumrev  15938  fsum0diag2  15942  binomlem  15991  climcndslem1  16011  climcndslem2  16012  harmonic  16021  mertenslem1  16046  fprodser  16109  fprodrev  16137  efcllem  16236  moddvds  16426  dvds1  16482  dvdsext  16484  evennn2n  16514  bitsinv1  16605  sadaddlem  16629  sadasslem  16633  sadeq  16635  mulgcd  16714  lcmftp  16804  rpmulgcd2  16824  coprmproddvdslem  16830  isprm5  16876  isprm6  16883  crth  16948  eulerthlem2  16952  prmdiveq  16956  pythagtriplem11  16996  pythagtriplem13  16998  pcgcd1  17048  pcprmpw2  17053  pcaddlem  17059  fldivp1  17068  4sqlem12  17127  4sqlem14  17129  4sqlem15  17130  4sqlem16  17131  vdwapun  17145  mreexexlem4d  17814  acsfn1  17828  acsfn2  17830  sscpwex  17983  rescabs  18001  yonedainv  18448  chnub  18789  subm0  19004  pmtrfb  19672  psgnunilem1  19700  odmodnn0  19747  odeq  19757  dfod2  19771  sylow1lem1  19805  lsmsubg  19861  lsmmod  19882  lsmdisj2  19889  ghmplusg  20053  odadd  20057  gexexlem  20059  lt6abl  20102  cyggex2  20104  dprdfinv  20228  dmdprdsplitlem  20246  dpjidcl  20267  ablfacrp  20275  ablfacrp2  20276  ablfac1c  20280  ablfac1eu  20282  omndadd2d  20337  omndadd2rd  20338  omndmul2  20340  acsfn1p  21049  lcomfsupp  21170  lssvancl1  21213  lssvnegcl  21224  lspprvacl  21267  ellspsni  21269  lspsn  21270  lmhmplusg  21312  lmhmima  21315  lmhmpreima  21316  reslmhm  21320  lbsind2  21349  lsmcl  21351  lsmelval2  21353  lsppreli  21358  lspprabs  21363  pj1lmhm  21368  lssvs0or  21381  lspabs3  21392  lspfixed  21399  lspexch  21400  lsmcv  21412  lspsolv  21414  lidlmcld  21499  drngnidl  21524  rhmpreimaidl  21564  rngqiprngimfo  21590  rngqiprngfulem4  21603  isprmidlc  21621  rhmpreimaprmidl  21628  qsidomlem1  21629  ssdifidllem  21633  gzrngunit  21732  zringlpirlem3  21763  prmirredlem  21771  znf1o  21850  znunithash  21863  freshmansdream  21873  ofldchr  21875  frlmsubgval  22064  frlmvplusgvalc  22066  frlmvscaval  22067  frlmphllem  22079  frlmphl  22080  frlmssuvc1  22093  frlmsslsp  22095  frlmup1  22097  frlmup2  22098  lindfind2  22117  lindfrn  22120  f1lindf  22121  islindf4  22137  mplbas2  22344  evlslem3  22382  evlslem1  22384  evladdval  22405  evlmulval  22406  evlsaddval  22431  evlsmulval  22432  coe1addfv  22577  lply1binom  22621  evl1addd  22652  evl1subd  22653  evl1muld  22654  mamudi  22711  mamudir  22712  1marepvmarrepid  22883  mdetrlin  22910  smadiadetglem1  22979  smadiadetg  22981  cramerimplem1  22994  mat2pmatscmxcl  23051  m2pmfzgsumcl  23059  pmatcollpw  23092  pmatcollpwfi  23093  pmatcollpw3fi1lem1  23097  cpmidpmatlem2  23182  cpmadugsumlemF  23187  chcoeffeqlem  23196  ntrin  23372  topssnei  23435  restbas  23469  restntr  23493  cnntri  23582  fiuncmp  23715  nllyrest  23798  nllyidm  23801  hausllycmp  23806  cldllycmp  23807  hauspwdom  23813  txcld  23915  txcn  23938  txlly  23948  txnlly  23949  txhaus  23959  txlm  23960  txkgen  23964  xkococnlem  23971  cnmpt2res  23989  xkoinjcn  23999  basqtop  24023  qtopeu  24028  trfbas2  24155  neifil  24192  hausflim  24293  alexsubALTlem2  24360  cnextfval  24374  cnextfvval  24377  cnextf  24378  cnextfres  24381  clssubg  24421  utop2nei  24562  utop3cls  24563  utopreg  24564  psmetlecl  24627  xmetlecl  24658  prdsxmetlem  24680  bldisj  24710  imasf1obl  24800  prdsbl  24803  stdbdmet  24828  stdbdmopn  24830  met2ndci  24834  metcnp  24853  metustto  24865  metustexhalf  24868  cfilucfil  24871  metucn  24883  lssnlm  25013  nmotri  25051  nmoid  25054  tgioo  25108  blcvx  25110  xrsmopn  25125  reperflem  25131  reconnlem2  25140  opnreen  25144  metdsge  25162  metdsre  25166  metdscnlem  25168  metnrmlem1a  25171  metnrmlem1  25172  metnrmlem3  25174  cncfmet  25223  cnmpopc  25242  icopnfcnv  25256  icopnfhmeo  25257  cnllycmp  25270  evth  25273  lebnumii  25280  nmoleub2lem3  25429  iscfil2  25580  cfil3i  25583  iscfil3  25587  cfilfcls  25588  iscau3  25592  iscmet3lem2  25606  caubl  25622  lmcau  25627  cssbn  25689  rrxcph  25706  minveclem2  25740  pjthlem1  25751  pjthlem2  25752  ivthicc  25772  ovollecl  25797  ovolunlem1a  25810  ovolunnul  25814  ovoliunlem1  25816  ismbl2  25841  nulmbl2  25850  unmbl  25851  volun  25859  voliunlem2  25865  ioombl1lem2  25873  uniioombllem2a  25896  uniioombllem3  25899  uniioombllem4  25900  dyaddisjlem  25909  dyadmaxlem  25911  opnmbllem  25915  volsup2  25919  volcn  25920  ismbfd  25953  mbfi1fseqlem1  26029  mbfi1fseqlem5  26033  itg2lecl  26052  itg2monolem2  26065  itg2gt0  26074  itgspliticc  26150  ellimc3  26192  limcres  26199  dvfval  26210  dvres3  26226  dvres3a  26227  dvmptresicc  26229  dvnff  26236  dvnadd  26242  dvn2bss  26243  dvnres  26244  dvcmul  26257  dvcmulf  26258  dvmptres3  26269  dvmptres2  26275  dvmptntr  26284  dvexp3  26291  dvferm1lem  26297  dvlip  26306  dvlipcn  26307  dvlip2  26308  c1liplem1  26309  dvgt0lem1  26315  dvgt0lem2  26316  dvne0  26324  lhop1lem  26326  lhop2  26328  lhop  26329  dvcnvrelem1  26330  dvcnvrelem2  26331  dvcvx  26333  dvfsumle  26334  dvfsumabs  26336  dvfsumlem2  26340  ftc1lem6  26354  ftc1  26355  ftc2ditglem  26358  itgsubstlem  26361  itgpowd  26363  tdeglem4  26371  mdegaddle  26385  mdegmullem  26389  ply1rem  26477  fta1glem2  26480  fta1blem  26482  ig1peu  26486  ig1pdvds  26491  dgrmulc  26583  dgrcolem1  26585  plydivlem4  26610  plydiveu  26612  fta1lem  26621  vieta1lem1  26626  vieta1lem2  26627  plyexmo  26629  taylfvallem1  26677  taylfval  26679  tayl0  26682  taylplem1  26683  taylply2  26688  taylply  26689  dvtaylp  26690  dvntaylp  26691  dvntaylp0  26692  taylthlem1  26693  taylthlem2  26694  ulmcaulem  26714  ulmcau  26715  ulmcn  26719  ulmdvlem1  26720  radcnvlem1  26733  radcnvle  26740  psercn  26746  pserdvlem2  26748  pserdv  26749  abelth  26761  tanregt0  26860  dvlog2lem  26973  efopn  26979  logtayllem  26980  logccv  26984  cxplt3  27021  cxpmul2zd  27037  cxpltd  27040  cxpled  27041  cxplt3d  27056  cxple3d  27057  dvsqrt  27063  cxpcn3  27069  cxpaddle  27073  cxpeq  27078  angcan  27123  angvald  27125  ang180lem2  27131  ang180  27135  isosctrlem3  27141  dquartlem1  27172  atantayl2  27259  leibpi  27263  log2tlbnd  27266  birthdaylem3  27274  xrlimcnp  27289  efrlim  27290  o1cxp  27295  jensenlem2  27308  jensen  27309  fsumharmonic  27332  lgamucov  27358  lgamcvg2  27375  wilthlem1  27388  basellem3  27403  basellem6  27406  basellem8  27408  ppisval  27424  chtwordi  27476  ppiwordi  27482  mumullem2  27500  mpodvdsmulf1o  27514  dvdsmulf1o  27516  fsumvma  27533  fsumvma2  27534  chpchtsum  27539  chpub  27540  logfacubnd  27541  dchrmulcl  27569  dchrinv  27581  dchrptlem1  27584  dchrptlem2  27585  sumdchr2  27590  dchr2sum  27593  bposlem7  27610  lgslem1  27617  lgslem3  27619  lgsdirprm  27651  lgsqrlem2  27667  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem4  27698  lgseisen  27699  lgsquadlem1  27700  lgsquad2lem1  27704  lgsquad3  27707  m1lgs  27708  2sqlem7  27744  2sq2  27753  2sqmod  27756  chebbnd1lem2  27790  chebbnd1lem3  27791  rplogsumlem1  27804  rpvmasumlem  27807  dchrvmasumlem1  27815  dchrvmasum2lem  27816  dchrvmasumlema  27820  dchrisum0flblem2  27829  dchrisum0fno1  27831  dchrisum0re  27833  logdivsum  27853  pntrsumbnd2  27887  pntpbnd1a  27905  pntpbnd1  27906  pntibndlem2  27911  pntlemr  27922  pntlemj  27923  pntlemf  27925  pnt2  27933  padicabv  27950  ostth2lem2  27954  lesrecd  28179  ltsrecd  28181  madebday  28279  addsproplem6  28353  negsproplem6  28412  mulsproplem13  28507  mulsproplem14  28508  ltmulsd  28516  mulsgt0d  28524  angmgmaddov2  29382  f1otrg  29441  brbtwn2  29476  colinearalglem2  29478  axcgrtr  29486  axcgrid  29487  axsegconlem7  29494  axsegcon  29498  ax5seglem3  29502  ax5seglem6  29505  ax5seg  29509  axpaschlem  29511  axlowdimlem17  29529  axcontlem2  29536  axcontlem4  29538  axcontlem7  29541  axcontlem8  29542  ecgrtg  29554  usgredg2v  29801  vtxdgoddnumeven  30127  2trlond  30521  eupthp1  30810  nmobndi  31370  ubthlem2  31466  ubthlem3  31467  minvecolem2  31470  shuni  31895  pjhthlem1  31986  chscllem2  32233  pjcompi  32267  mayete3i  32323  unoplin  32515  hmoplin  32537  nmophmi  32626  mdslmd4i  32928  isoun  33288  submuladdd  33325  receqid  33329  xrge0addcld  33347  xrofsup  33352  eliccelico  33362  elicoelioo  33363  difioo  33367  rexdiv  33485  mgcmnt1d  33551  mgcmnt2d  33552  xrge0addgt0  33571  cycpmcl  33670  cycpm2tr  33673  cyc3evpm  33704  cycpmconjslem2  33709  fldgensdrg  33869  qusker  33903  eqgvscpbl  33904  ringlsmss1  33942  ringlsmss2  33943  intlidl  33963  lidlunitel  33966  elrspunidl  33971  idlinsubrg  33974  mxidlmaxv  33986  mxidlprm  33988  ssmxidllem  33991  opprmxidlabs  34004  qsdrnglem2  34013  dflring3  34022  dflring4  34023  selvply1rhmlem4  34148  mplvrpmmhm  34171  mplvrpmrhm  34172  esplyind  34200  resssra  34212  ply1degltdimlem  34247  lindsunlem  34249  sdrgfldext  34275  fldsdrgfldext  34286  finexttrb  34290  fldgenfldext  34293  fldextrspunlem1  34300  algextdeglem4  34345  algextdeglem8  34349  constrextdg2lem  34373  mdetpmtr2  34449  mdetpmtr12  34450  madjusmdetlem1  34452  madjusmdetlem4  34455  rhmpreimacn  34510  unitdivcld  34526  xrge0mulc1cn  34566  qqhnm  34615  esumcst  34688  esumfsup  34695  esumpmono  34704  esumcvg  34711  sigapisys  34781  sigapildsys  34788  ldgenpisyslem1  34789  1stmbfm  34885  2ndmbfm  34886  dya2icoseg  34902  sibfinima  34964  probmeasb  35055  orvcgteel  35093  orvclteel  35098  ballotlemsima  35141  ballotlemfrceq  35154  ccatmulgnn0dir  35167  fct2relem  35219  ftc2re  35220  chtvalz  35251  subfacp1lem2a  35924  subfaclim  35932  erdsze2lem2  35948  cvmliftlem2  36030  cvmliftlem10  36038  cvmliftlem13  36040  cvmliftiota  36045  cvmlift2lem9  36055  cvmlift2lem11  36057  cvmlift2lem12  36058  cvmliftphtlem  36061  cvmlift3lem6  36068  cvmlift3lem7  36069  cvmlift3lem9  36071  snmlff  36073  mrsubfval  36252  wzel  36566  wsuclem  36567  brsegle  36853  nmulel1  36944  nadddilem1  36949  nadddilem3  36951  opnregcld  37098  weiunfrlem  37232  fin2so  38510  poimirlem17  38535  poimirlem23  38541  opnmbllem0  38554  mblfinlem3  38557  mblfinlem4  38558  itg2addnclem  38569  itg2addnc  38572  itg2gt0cn  38573  ftc1cnnclem  38589  ftc1cnnc  38590  areacirclem5  38610  indexdom  38648  sstotbnd2  38688  isbnd3  38698  isbnd3b  38699  cntotbnd  38710  ismtyima  38717  heibor1lem  38723  heiborlem8  38732  rrncmslem  38746  reheibor  38753  lkrlsp  40139  lshpkrlem5  40151  ldualssvscl  40195  ldualssvsubcl  40196  llnmlplnN  40576  llncvrlpln  40595  pmapjat1  40890  pclfinN  40937  lautlt  41128  lauteq  41132  lautco  41134  ltrn11  41163  ltrnle  41166  ltrneq2  41185  cdlemednuN  41337  cdleme20k  41356  cdleme20l2  41358  cdleme20l  41359  cdleme20m  41360  cdleme21c  41364  cdleme22e  41381  cdleme22eALTN  41382  cdlemefrs32fva  41437  cdlemg4g  41653  cdlemg18b  41716  cdlemg18c  41717  cdlemj3  41860  dia2dimlem5  42105  dvhopN  42153  cdlemm10N  42155  dihjatcclem4  42458  dochexmidlem2  42498  lclkrlem2o  42558  lcfrlem5  42583  lcfrlem6  42584  lcdlssvscl  42643  mapdpglem6  42715  mapdpglem9  42717  mapdpglem12  42720  mapdpglem14  42722  mapdindp0  42756  hdmaprnlem7N  42892  hdmaprnlem8N  42893  hdmaprnlem3eN  42895  hgmapvvlem3  42962  dvun  43390  addinvcom  43463  mzpsubst  43738  eldioph2lem1  43750  eldioph2lem2  43751  eldioph2b  43753  diophin  43762  irrapxlem2  43809  irrapxlem4  43811  irrapxlem5  43812  pellexlem1  43815  pellexlem2  43816  pellexlem6  43820  elpell1qr2  43858  pell1qrgaplem  43859  pell1qrgap  43860  pellqrex  43865  pellfundex  43872  pellfund14  43884  rmspecsqrtnq  43892  rmxyadd  43907  congsub  43956  mzpcong  43958  congrep  43959  acongtr  43964  acongrep  43966  jm2.19lem1  43975  jm2.22  43981  jm2.23  43982  jm2.26lem3  43987  jm2.26  43988  jm2.27a  43991  fnwe2lem2  44037  aomclem6  44045  hbtlem2  44110  hbtlem4  44112  hbtlem5  44114  dgraa0p  44135  rngunsnply  44155  proot1hash  44181  nnoeomeqom  44298  cantnf2  44311  omabs2  44318  naddcnff  44348  naddcnffo  44350  naddcnfcom  44352  naddcnfid1  44353  expgrowth  45304  fpmd  46244  abslt2sqd  46341  ioondisj2  46474  ioondisj1  46475  eliocre  46490  ioossioobi  46498  iooiinicc  46523  iooiinioc  46537  lptioo2  46612  limcresiooub  46621  limsupequzlem  46701  xlimmnfvlem2  46812  xlimpnfvlem2  46816  cncfuni  46865  cncfiooicclem1  46872  cxpcncf2  46878  dvcnre  46895  dvresntr  46897  dvresioo  46900  dvbdfbdioolem1  46907  dvnmptdivc  46917  dvnxpaek  46921  itgsinexplem1  46933  itgcoscmulx  46948  itgiccshift  46959  itgperiod  46960  ovolsplit  46967  stoweidlem11  46990  stoweidlem26  47005  stoweidlem34  47013  stoweidlem36  47015  stoweidlem38  47017  stirlinglem5  47057  dirkercncflem2  47083  dirkercncflem4  47085  fourierdlem20  47106  fourierdlem58  47143  fourierdlem72  47157  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem79  47164  fourierdlem80  47165  fourierdlem87  47172  fourierdlem94  47179  fourierdlem103  47188  fourierdlem104  47189  fourierdlem107  47192  fourierdlem113  47198  sqwvfoura  47207  sqwvfourb  47208  fourierswlem  47209  fouriersw  47210  etransclem46  47259  etransclem47  47260  rrndistlt  47269  rrnprjdstle  47280  ioorrnopnxrlem  47285  sge0ssre  47376  sge0seq  47425  hsphoidmvle2  47564  hsphoidmvle  47565  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmv1lelem3  47572  hoidmvlelem1  47574  hoidifhspdmvle  47599  hoiqssbllem2  47602  ovolval5lem2  47632  iinhoiicc  47653  iunhoiioo  47655  vonioolem2  47660  vonicclem2  47663  issmflem  47706  sqrtnnaa  47882  submodlt  48395  iccpartdisj  48488  m1expevenALTV  48714  fpprel2  48808  tgoldbach  48884  opstrgric  48993  gpg3kgrtriex  49156  nn0eo  49609  fdivpm  49624  refdivpm  49625  elbigolo1  49638  logbpw2m1  49648  fllog2  49649  dignn0flhalflem1  49696  dignn0flhalflem2  49697  itsclinecirc0in  49856  2itscplem2  49860  itscnhlinecirc02plem1  49863  iccdisj2  49974