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  4826  fr2nr  5640  soltmin  6138  f1oprg  6871  f1prex  7291  fveqf1o  7309  weniso  7363  fr3nr  7777  suppofssd  8205  smogt  8360  smocdmdom  8361  oacomf1o  8556  en2prd  9051  difsnen  9054  enfixsn  9081  domss2  9131  ssenen  9146  marypha1lem  9400  fisupcl  9437  ordtypelem3  9489  ordtypelem8  9494  oieu  9508  oismo  9509  wofib  9514  wemaplem2  9516  wemapso  9520  wemapso2lem  9521  unxpwdom2  9557  infdifsn  9633  oemapvali  9660  cantnflem1c  9663  cantnflem1  9665  cantnf  9669  cnfcom3  9680  r1ordg  9757  dif1card  10010  infxpenlem  10013  dfac8clem  10032  infxp  10213  infmap2  10216  cflim2  10262  coftr  10272  fin2i2  10317  enfin2i  10320  fin23lem26  10324  fin23lem27  10327  fin23lem40  10350  isf32lem2  10353  isf32lem3  10354  isf32lem4  10355  isf32lem7  10358  isf32lem9  10360  fin1a2lem13  10411  fin12  10412  alephexp1  10579  gchdomtri  10629  fpwwe2lem11  10641  fpwwe2lem12  10642  gchpwdom  10670  gchhar  10679  adderpqlem  10954  mulerpqlem  10955  addassnq  10958  mulassnq  10959  distrnq  10961  mulidnq  10963  recmulnq  10964  ltexnq  10975  distrlem1pr  11025  distrlem4pr  11026  prlem936  11047  reclem3pr  11049  mulcmpblnr  11071  mulgt0d  11380  mul4d  11437  add4d  11454  add42d  11455  subcan  11528  addsub4d  11631  subadd4d  11632  sub4d  11633  2addsubd  11634  addsubeq4d  11635  muladdd  11687  mulsubd  11688  addgegt0d  11802  addgtge0d  11803  addge0d  11805  mulge0d  11806  le2subd  11849  ltleaddd  11850  leltaddd  11851  lt2subd  11853  divdivdiv  11931  divcan5  11932  divne0d  12022  recdivd  12023  recdiv2d  12024  divcan6d  12025  ddcand  12026  rec11d  12027  divmuldivd  12047  divmul13d  12048  divmul24d  12049  divadddivd  12050  divsubdivd  12051  divmuleqd  12052  divdivdivd  12053  mulge0b  12100  recreclt  12129  divgt0d  12165  mulgt1d  12166  lemulge11d  12167  lemulge12d  12168  ltmul12ad  12171  lemul12ad  12172  lemul12bd  12173  supmul1  12199  nndivtr  12298  qreccl  13009  ledivdivd  13101  lediv12ad  13135  lt2mul2divd  13145  xlt2add  13302  supxrun  13358  supxrre  13369  infxrre  13379  elicore  13441  iccss2  13460  iccssico2  13463  icossico2d  13464  lincmb01cmp  13538  iccf1o  13539  nnge2recico01  13550  fzrev2i  13634  2tnp1ge0ge0  13880  m1modnnsub1  13971  modaddmodup  13988  modaddmodlo  13989  modsubdir  13994  fzennn  14022  sermono  14088  mulexpz  14156  expaddz  14160  sqdiv  14175  expsubd  14211  ltexp2a  14220  expmordi  14221  leexp2a  14226  expmulnbnd  14289  digit1  14291  lt2sqd  14310  le2sqd  14311  sq11d  14312  bcm1k  14369  bcp1n  14370  bcp1nk  14371  hashpss  14464  hashf1lem1  14510  cshw1  14883  2swrd2eqwrdeq  15014  ofccat  15030  sgnmul  15168  absrele  15383  sqreulem  15435  sqrtmuld  15500  sqrtsq2d  15501  sqrtled  15502  sqrtltd  15503  sqr11d  15504  abs3lemd  15539  rlimuni  15625  climuni  15627  lo1resb  15639  o1resb  15641  2clim  15647  addcn2  15669  mulcn2  15671  o1of2  15688  o1rlimmul  15694  lo1add  15702  lo1mul  15703  isercolllem1  15740  caucvgrlem  15748  iseraltlem2  15758  iseraltlem3  15759  mptfzshft  15852  fsumrev  15853  fsum0diag2  15857  binomlem  15906  climcndslem1  15926  climcndslem2  15927  harmonic  15936  mertenslem1  15961  fprodser  16026  fprodrev  16054  efcllem  16153  moddvds  16343  dvds1  16399  dvdsext  16401  evennn2n  16431  bitsinv1  16522  sadaddlem  16546  sadasslem  16550  sadeq  16552  mulgcd  16628  dvdssqlem  16646  lcmftp  16716  rpmulgcd2  16736  coprmproddvdslem  16742  isprm5  16788  isprm6  16795  crth  16859  eulerthlem2  16863  prmdiveq  16867  pythagtriplem11  16907  pythagtriplem13  16909  pcgcd1  16959  pcprmpw2  16964  pcaddlem  16970  fldivp1  16979  4sqlem12  17038  4sqlem14  17040  4sqlem15  17041  4sqlem16  17042  vdwapun  17056  mreexexlem4d  17725  acsfn1  17739  acsfn2  17741  sscpwex  17894  rescabs  17912  yonedainv  18359  chnub  18700  subm0  18911  pmtrfb  19579  psgnunilem1  19607  odmodnn0  19654  odeq  19664  dfod2  19678  sylow1lem1  19712  lsmsubg  19768  lsmmod  19789  lsmdisj2  19796  ghmplusg  19960  odadd  19964  gexexlem  19966  lt6abl  20009  cyggex2  20011  dprdfinv  20135  dmdprdsplitlem  20153  dpjidcl  20174  ablfacrp  20182  ablfacrp2  20183  ablfac1c  20187  ablfac1eu  20189  omndadd2d  20244  omndadd2rd  20245  omndmul2  20247  acsfn1p  20952  lcomfsupp  21073  lssvancl1  21116  lssvnegcl  21127  lspprvacl  21170  ellspsni  21172  lspsn  21173  lmhmplusg  21215  lmhmima  21218  lmhmpreima  21219  reslmhm  21223  lbsind2  21252  lsmcl  21254  lsmelval2  21256  lsppreli  21261  lspprabs  21266  pj1lmhm  21271  lssvs0or  21284  lspabs3  21295  lspfixed  21302  lspexch  21303  lsmcv  21315  lspsolv  21317  lidlmcld  21402  drngnidl  21427  rhmpreimaidl  21466  rngqiprngimfo  21491  rngqiprngfulem4  21504  isprmidlc  21522  rhmpreimaprmidl  21529  qsidomlem1  21530  ssdifidllem  21534  gzrngunit  21633  zringlpirlem3  21664  prmirredlem  21672  znf1o  21751  znunithash  21764  freshmansdream  21774  ofldchr  21776  frlmsubgval  21965  frlmvplusgvalc  21967  frlmvscaval  21968  frlmphllem  21980  frlmphl  21981  frlmssuvc1  21994  frlmsslsp  21996  frlmup1  21998  frlmup2  21999  lindfind2  22018  lindfrn  22021  f1lindf  22022  islindf4  22038  mplbas2  22243  evlslem3  22281  evlslem1  22283  evladdval  22304  evlmulval  22305  evlsaddval  22330  evlsmulval  22331  coe1addfv  22476  lply1binom  22520  evl1addd  22551  evl1subd  22552  evl1muld  22553  mamudi  22610  mamudir  22611  1marepvmarrepid  22782  mdetrlin  22809  smadiadetglem1  22878  smadiadetg  22880  cramerimplem1  22890  mat2pmatscmxcl  22947  m2pmfzgsumcl  22955  pmatcollpw  22988  pmatcollpwfi  22989  pmatcollpw3fi1lem1  22993  cpmidpmatlem2  23078  cpmadugsumlemF  23083  chcoeffeqlem  23092  ntrin  23268  topssnei  23331  restbas  23365  restntr  23389  cnntri  23478  fiuncmp  23611  nllyrest  23694  nllyidm  23697  hausllycmp  23702  cldllycmp  23703  hauspwdom  23709  txcld  23811  txcn  23834  txlly  23844  txnlly  23845  txhaus  23855  txlm  23856  txkgen  23860  xkococnlem  23867  cnmpt2res  23885  xkoinjcn  23895  basqtop  23919  qtopeu  23924  trfbas2  24051  neifil  24088  hausflim  24189  alexsubALTlem2  24256  cnextfval  24270  cnextfvval  24273  cnextf  24274  cnextfres  24277  clssubg  24317  utop2nei  24458  utop3cls  24459  utopreg  24460  psmetlecl  24523  xmetlecl  24554  prdsxmetlem  24576  bldisj  24606  imasf1obl  24696  prdsbl  24699  stdbdmet  24724  stdbdmopn  24726  met2ndci  24730  metcnp  24749  metustto  24761  metustexhalf  24764  cfilucfil  24767  metucn  24779  lssnlm  24909  nmotri  24947  nmoid  24950  tgioo  25004  blcvx  25006  xrsmopn  25021  reperflem  25027  reconnlem2  25036  opnreen  25040  metdsge  25058  metdsre  25062  metdscnlem  25064  metnrmlem1a  25067  metnrmlem1  25068  metnrmlem3  25070  cncfmet  25119  cnmpopc  25138  icopnfcnv  25152  icopnfhmeo  25153  cnllycmp  25166  evth  25169  lebnumii  25176  nmoleub2lem3  25325  iscfil2  25476  cfil3i  25479  iscfil3  25483  cfilfcls  25484  iscau3  25488  iscmet3lem2  25502  caubl  25518  lmcau  25523  cssbn  25585  rrxcph  25602  minveclem2  25636  pjthlem1  25647  pjthlem2  25648  ivthicc  25668  ovollecl  25693  ovolunlem1a  25706  ovolunnul  25710  ovoliunlem1  25712  ismbl2  25737  nulmbl2  25746  unmbl  25747  volun  25755  voliunlem2  25761  ioombl1lem2  25769  uniioombllem2a  25792  uniioombllem3  25795  uniioombllem4  25796  dyaddisjlem  25805  dyadmaxlem  25807  opnmbllem  25811  volsup2  25815  volcn  25816  ismbfd  25849  mbfi1fseqlem1  25925  mbfi1fseqlem5  25929  itg2lecl  25948  itg2monolem2  25961  itg2gt0  25970  itgspliticc  26047  ellimc3  26089  limcres  26096  dvfval  26107  dvres3  26123  dvres3a  26124  dvmptresicc  26126  dvnff  26133  dvnadd  26139  dvn2bss  26140  dvnres  26141  dvcmul  26154  dvcmulf  26155  dvmptres3  26166  dvmptres2  26172  dvmptntr  26181  dvexp3  26188  dvferm1lem  26194  dvlip  26203  dvlipcn  26204  dvlip2  26205  c1liplem1  26206  dvgt0lem1  26212  dvgt0lem2  26213  dvne0  26221  lhop1lem  26223  lhop2  26225  lhop  26226  dvcnvrelem1  26227  dvcnvrelem2  26228  dvcvx  26230  dvfsumle  26231  dvfsumabs  26233  dvfsumlem2  26237  ftc1lem6  26251  ftc1  26252  ftc2ditglem  26255  itgsubstlem  26258  itgpowd  26260  tdeglem4  26268  mdegaddle  26282  mdegmullem  26286  ply1rem  26374  fta1glem2  26377  fta1blem  26379  ig1peu  26383  ig1pdvds  26388  dgrmulc  26479  dgrcolem1  26481  plydivlem4  26508  plydiveu  26510  fta1lem  26519  vieta1lem1  26522  vieta1lem2  26523  plyexmo  26525  taylfvallem1  26571  taylfval  26573  tayl0  26576  taylplem1  26577  taylply2  26582  taylply  26583  dvtaylp  26584  dvntaylp  26585  dvntaylp0  26586  taylthlem1  26587  taylthlem2  26588  ulmcaulem  26608  ulmcau  26609  ulmcn  26613  ulmdvlem1  26614  radcnvlem1  26627  radcnvle  26634  psercn  26640  pserdvlem2  26642  pserdv  26643  abelth  26655  tanregt0  26755  dvlog2lem  26868  efopn  26874  logtayllem  26875  logccv  26879  cxplt3  26916  cxpmul2zd  26932  cxpltd  26935  cxpled  26936  cxplt3d  26951  cxple3d  26952  dvsqrt  26958  cxpcn3  26964  cxpaddle  26968  cxpeq  26973  angcan  27018  angvald  27020  ang180lem2  27026  ang180  27030  isosctrlem3  27036  dquartlem1  27067  atantayl2  27154  leibpi  27158  log2tlbnd  27161  birthdaylem3  27169  xrlimcnp  27184  efrlim  27185  o1cxp  27190  jensenlem2  27203  jensen  27204  fsumharmonic  27227  lgamucov  27253  lgamcvg2  27270  wilthlem1  27283  basellem3  27298  basellem6  27301  basellem8  27303  ppisval  27319  chtwordi  27371  ppiwordi  27377  mumullem2  27395  mpodvdsmulf1o  27409  dvdsmulf1o  27411  fsumvma  27428  fsumvma2  27429  chpchtsum  27434  chpub  27435  logfacubnd  27436  dchrmulcl  27464  dchrinv  27476  dchrptlem1  27479  dchrptlem2  27480  sumdchr2  27485  dchr2sum  27488  bposlem7  27505  lgslem1  27512  lgslem3  27514  lgsdirprm  27546  lgsqrlem2  27562  lgseisenlem1  27590  lgseisenlem2  27591  lgseisenlem4  27593  lgseisen  27594  lgsquadlem1  27595  lgsquad2lem1  27599  lgsquad3  27602  m1lgs  27603  2sqlem7  27639  2sq2  27648  2sqmod  27651  chebbnd1lem2  27685  chebbnd1lem3  27686  rplogsumlem1  27699  rpvmasumlem  27702  dchrvmasumlem1  27710  dchrvmasum2lem  27711  dchrvmasumlema  27715  dchrisum0flblem2  27724  dchrisum0fno1  27726  dchrisum0re  27728  logdivsum  27748  pntrsumbnd2  27782  pntpbnd1a  27800  pntpbnd1  27801  pntibndlem2  27806  pntlemr  27817  pntlemj  27818  pntlemf  27820  pnt2  27828  padicabv  27845  ostth2lem2  27849  lesrecd  28044  ltsrecd  28046  madebday  28144  addsproplem6  28218  negsproplem6  28277  mulsproplem13  28372  mulsproplem14  28373  ltmulsd  28381  mulsgt0d  28389  f1otrg  29275  brbtwn2  29310  colinearalglem2  29312  axcgrtr  29320  axcgrid  29321  axsegconlem7  29328  axsegcon  29332  ax5seglem3  29336  ax5seglem6  29339  ax5seg  29343  axpaschlem  29345  axlowdimlem17  29363  axcontlem2  29370  axcontlem4  29372  axcontlem7  29375  axcontlem8  29376  ecgrtg  29388  usgredg2v  29635  vtxdgoddnumeven  29961  2trlond  30355  eupthp1  30638  nmobndi  31198  ubthlem2  31294  ubthlem3  31295  minvecolem2  31298  shuni  31723  pjhthlem1  31814  chscllem2  32061  pjcompi  32095  mayete3i  32151  unoplin  32343  hmoplin  32365  nmophmi  32454  mdslmd4i  32756  isoun  33118  submuladdd  33155  receqid  33159  xrge0addcld  33177  xrofsup  33182  eliccelico  33192  elicoelioo  33193  difioo  33197  rexdiv  33315  mgcmnt1d  33381  mgcmnt2d  33382  xrge0addgt0  33401  cycpmcl  33500  cycpm2tr  33503  cyc3evpm  33534  cycpmconjslem2  33539  fldgensdrg  33699  qusker  33733  eqgvscpbl  33734  ringlsmss1  33771  ringlsmss2  33772  intlidl  33792  lidlunitel  33795  elrspunidl  33800  idlinsubrg  33803  mxidlmaxv  33815  mxidlprm  33817  ssmxidllem  33820  opprmxidlabs  33833  qsdrnglem2  33842  dflring3  33851  dflring4  33852  selvply1rhmlem4  33977  mplvrpmmhm  34000  mplvrpmrhm  34001  esplyind  34029  resssra  34041  ply1degltdimlem  34076  lindsunlem  34078  sdrgfldext  34104  fldsdrgfldext  34115  finexttrb  34119  fldgenfldext  34122  fldextrspunlem1  34129  algextdeglem4  34174  algextdeglem8  34178  constrextdg2lem  34202  mdetpmtr2  34278  mdetpmtr12  34279  madjusmdetlem1  34281  madjusmdetlem4  34284  rhmpreimacn  34339  unitdivcld  34355  xrge0mulc1cn  34395  qqhnm  34444  esumcst  34517  esumfsup  34524  esumpmono  34533  esumcvg  34540  sigapisys  34610  sigapildsys  34617  ldgenpisyslem1  34618  1stmbfm  34715  2ndmbfm  34716  dya2icoseg  34732  sibfinima  34794  probmeasb  34885  orvcgteel  34923  orvclteel  34928  ballotlemsima  34971  ballotlemfrceq  34984  ccatmulgnn0dir  34997  fct2relem  35049  ftc2re  35050  chtvalz  35081  r1filimi  35555  subfacp1lem2a  35709  subfaclim  35717  erdsze2lem2  35733  cvmliftlem2  35815  cvmliftlem10  35823  cvmliftlem13  35825  cvmliftiota  35830  cvmlift2lem9  35840  cvmlift2lem11  35842  cvmlift2lem12  35843  cvmliftphtlem  35846  cvmlift3lem6  35853  cvmlift3lem7  35854  cvmlift3lem9  35856  snmlff  35858  mrsubfval  36037  wzel  36351  wsuclem  36352  brsegle  36637  nmulel1  36744  nadddilem1  36749  nadddilem3  36751  opnregcld  36898  weiunfrlem  37032  fin2so  38315  poimirlem17  38345  poimirlem23  38351  opnmbllem0  38364  mblfinlem3  38367  mblfinlem4  38368  itg2addnclem  38379  itg2addnc  38382  itg2gt0cn  38383  ftc1cnnclem  38399  ftc1cnnc  38400  areacirclem5  38420  indexdom  38443  sstotbnd2  38483  isbnd3  38493  isbnd3b  38494  cntotbnd  38505  ismtyima  38512  heibor1lem  38518  heiborlem8  38527  rrncmslem  38541  reheibor  38548  lkrlsp  39934  lshpkrlem5  39946  ldualssvscl  39990  ldualssvsubcl  39991  llnmlplnN  40371  llncvrlpln  40390  pmapjat1  40685  pclfinN  40732  lautlt  40923  lauteq  40927  lautco  40929  ltrn11  40958  ltrnle  40961  ltrneq2  40980  cdlemednuN  41132  cdleme20k  41151  cdleme20l2  41153  cdleme20l  41154  cdleme20m  41155  cdleme21c  41159  cdleme22e  41176  cdleme22eALTN  41177  cdlemefrs32fva  41232  cdlemg4g  41448  cdlemg18b  41511  cdlemg18c  41512  cdlemj3  41655  dia2dimlem5  41900  dvhopN  41948  cdlemm10N  41950  dihjatcclem4  42253  dochexmidlem2  42293  lclkrlem2o  42353  lcfrlem5  42378  lcfrlem6  42379  lcdlssvscl  42438  mapdpglem6  42510  mapdpglem9  42512  mapdpglem12  42515  mapdpglem14  42517  mapdindp0  42551  hdmaprnlem7N  42687  hdmaprnlem8N  42688  hdmaprnlem3eN  42690  hgmapvvlem3  42757  dvun  43178  addinvcom  43251  mzpsubst  43537  eldioph2lem1  43549  eldioph2lem2  43550  eldioph2b  43552  diophin  43561  irrapxlem2  43608  irrapxlem4  43610  irrapxlem5  43611  pellexlem1  43614  pellexlem2  43615  pellexlem6  43619  elpell1qr2  43657  pell1qrgaplem  43658  pell1qrgap  43659  pellqrex  43664  pellfundex  43671  pellfund14  43683  rmspecsqrtnq  43691  rmxyadd  43706  congsub  43755  mzpcong  43757  congrep  43758  acongtr  43763  acongrep  43765  jm2.19lem1  43774  jm2.22  43780  jm2.23  43781  jm2.26lem3  43786  jm2.26  43787  jm2.27a  43790  fnwe2lem2  43836  aomclem6  43844  hbtlem2  43909  hbtlem4  43911  hbtlem5  43913  dgraa0p  43934  rngunsnply  43954  proot1hash  43980  nnoeomeqom  44097  cantnf2  44110  omabs2  44117  naddcnff  44147  naddcnffo  44149  naddcnfcom  44151  naddcnfid1  44152  expgrowth  45103  fpmd  46036  abslt2sqd  46134  ioondisj2  46267  ioondisj1  46268  eliocre  46283  ioossioobi  46291  iooiinicc  46316  iooiinioc  46330  lptioo2  46405  limcresiooub  46414  limsupequzlem  46494  xlimmnfvlem2  46605  xlimpnfvlem2  46609  cncfuni  46658  cncfiooicclem1  46665  cxpcncf2  46671  dvcnre  46688  dvresntr  46690  dvresioo  46693  dvbdfbdioolem1  46700  dvnmptdivc  46710  dvnxpaek  46714  itgsinexplem1  46726  itgcoscmulx  46741  itgiccshift  46752  itgperiod  46753  ovolsplit  46760  stoweidlem11  46783  stoweidlem26  46798  stoweidlem34  46806  stoweidlem36  46808  stoweidlem38  46810  stirlinglem5  46850  dirkercncflem2  46876  dirkercncflem4  46878  fourierdlem20  46899  fourierdlem58  46936  fourierdlem72  46950  fourierdlem73  46951  fourierdlem74  46952  fourierdlem75  46953  fourierdlem76  46954  fourierdlem79  46957  fourierdlem80  46958  fourierdlem87  46965  fourierdlem94  46972  fourierdlem103  46981  fourierdlem104  46982  fourierdlem107  46985  fourierdlem113  46991  sqwvfoura  47000  sqwvfourb  47001  fourierswlem  47002  fouriersw  47003  etransclem46  47052  etransclem47  47053  rrndistlt  47062  rrnprjdstle  47073  ioorrnopnxrlem  47078  sge0ssre  47169  sge0seq  47218  hsphoidmvle2  47357  hsphoidmvle  47358  hoidmv1lelem1  47363  hoidmv1lelem2  47364  hoidmv1lelem3  47365  hoidmvlelem1  47367  hoidifhspdmvle  47392  hoiqssbllem2  47395  ovolval5lem2  47425  iinhoiicc  47446  iunhoiioo  47448  vonioolem2  47453  vonicclem2  47456  issmflem  47499  submodlt  48151  iccpartdisj  48244  m1expevenALTV  48470  fpprel2  48564  tgoldbach  48640  opstrgric  48749  gpg3kgrtriex  48912  nn0eo  49365  fdivpm  49380  refdivpm  49381  elbigolo1  49394  logbpw2m1  49404  fllog2  49405  dignn0flhalflem1  49452  dignn0flhalflem2  49453  itsclinecirc0in  49612  2itscplem2  49616  itscnhlinecirc02plem1  49619  iccdisj2  49732