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  4823  fr2nr  5615  soltmin  6109  f1oprg  6845  f1prex  7259  fveqf1o  7277  weniso  7329  fr3nr  7748  suppofssd  8182  smogt  8336  smocdmdom  8337  oacomf1o  8529  en2prd  9019  enpr2dOLD  9021  difsnen  9023  enfixsn  9050  domss2  9100  ssenen  9115  marypha1lem  9384  fisupcl  9421  ordtypelem3  9473  ordtypelem8  9478  oieu  9492  oismo  9493  wofib  9498  wemaplem2  9500  wemapso  9504  wemapso2lem  9505  unxpwdom2  9541  infdifsn  9610  oemapvali  9637  cantnflem1c  9640  cantnflem1  9642  cantnf  9646  cnfcom3  9657  r1ordg  9731  dif1card  9963  infxpenlem  9966  dfac8clem  9985  infxp  10167  infmap2  10170  cflim2  10216  coftr  10226  fin2i2  10271  enfin2i  10274  fin23lem26  10278  fin23lem27  10281  fin23lem40  10304  isf32lem2  10307  isf32lem3  10308  isf32lem4  10309  isf32lem7  10312  isf32lem9  10314  fin1a2lem13  10365  fin12  10366  alephexp1  10532  gchdomtri  10582  fpwwe2lem11  10594  fpwwe2lem12  10595  gchpwdom  10623  gchhar  10632  adderpqlem  10907  mulerpqlem  10908  addassnq  10911  mulassnq  10912  distrnq  10914  mulidnq  10916  recmulnq  10917  ltexnq  10928  distrlem1pr  10978  distrlem4pr  10979  prlem936  11000  reclem3pr  11002  mulcmpblnr  11024  mulgt0d  11329  mul4d  11386  add4d  11403  add42d  11404  subcan  11477  addsub4d  11580  subadd4d  11581  sub4d  11582  2addsubd  11583  addsubeq4d  11584  muladdd  11636  mulsubd  11637  addgegt0d  11751  addgtge0d  11752  addge0d  11754  mulge0d  11755  le2subd  11798  ltleaddd  11799  leltaddd  11800  lt2subd  11802  divdivdiv  11883  divcan5  11884  divne0d  11974  recdivd  11975  recdiv2d  11976  divcan6d  11977  ddcand  11978  rec11d  11979  divmuldivd  11999  divmul13d  12000  divmul24d  12001  divadddivd  12002  divsubdivd  12003  divmuleqd  12004  divdivdivd  12005  mulge0b  12053  recreclt  12082  divgt0d  12118  mulgt1d  12119  lemulge11d  12120  lemulge12d  12121  ltmul12ad  12124  lemul12ad  12125  lemul12bd  12126  supmul1  12152  nndivtr  12233  qreccl  12928  ledivdivd  13020  lediv12ad  13054  lt2mul2divd  13064  xlt2add  13220  supxrun  13276  supxrre  13287  infxrre  13297  elicore  13359  iccss2  13378  iccssico2  13381  icossico2d  13382  lincmb01cmp  13456  iccf1o  13457  fzrev2i  13550  2tnp1ge0ge0  13791  m1modnnsub1  13882  modaddmodup  13899  modaddmodlo  13900  modsubdir  13905  fzennn  13933  sermono  13999  mulexpz  14067  expaddz  14071  sqdiv  14086  expsubd  14122  ltexp2a  14131  expmordi  14132  leexp2a  14137  expmulnbnd  14200  digit1  14202  lt2sqd  14221  le2sqd  14222  sq11d  14223  bcm1k  14280  bcp1n  14281  bcp1nk  14282  hashf1lem1  14420  cshw1  14787  2swrd2eqwrdeq  14919  ofccat  14935  absrele  15274  sqreulem  15326  sqrtmuld  15391  sqrtsq2d  15392  sqrtled  15393  sqrtltd  15394  sqr11d  15395  abs3lemd  15430  rlimuni  15516  climuni  15518  lo1resb  15530  o1resb  15532  2clim  15538  addcn2  15560  mulcn2  15562  o1of2  15579  o1rlimmul  15585  lo1add  15593  lo1mul  15594  isercolllem1  15631  caucvgrlem  15639  iseraltlem2  15649  iseraltlem3  15650  mptfzshft  15744  fsumrev  15745  fsum0diag2  15749  binomlem  15795  climcndslem1  15815  climcndslem2  15816  harmonic  15825  mertenslem1  15850  fprodser  15915  fprodrev  15943  efcllem  16043  moddvds  16233  dvds1  16289  dvdsext  16291  evennn2n  16321  bitsinv1  16412  sadaddlem  16436  sadasslem  16440  sadeq  16442  mulgcd  16518  dvdssqlem  16536  lcmftp  16606  rpmulgcd2  16626  coprmproddvdslem  16632  isprm5  16677  isprm6  16684  crth  16748  eulerthlem2  16752  prmdiveq  16756  pythagtriplem11  16796  pythagtriplem13  16798  pcgcd1  16848  pcprmpw2  16853  pcaddlem  16859  fldivp1  16868  4sqlem12  16927  4sqlem14  16929  4sqlem15  16930  4sqlem16  16931  vdwapun  16945  mreexexlem4d  17608  acsfn1  17622  acsfn2  17624  sscpwex  17777  rescabs  17795  yonedainv  18242  subm0  18742  pmtrfb  19395  psgnunilem1  19423  odmodnn0  19470  odeq  19480  dfod2  19494  sylow1lem1  19528  lsmsubg  19584  lsmmod  19605  lsmdisj2  19612  ghmplusg  19776  odadd  19780  gexexlem  19782  lt6abl  19825  cyggex2  19827  dprdfinv  19951  dmdprdsplitlem  19969  dpjidcl  19990  ablfacrp  19998  ablfacrp2  19999  ablfac1c  20003  ablfac1eu  20005  acsfn1p  20708  lcomfsupp  20808  lssvancl1  20851  lssvnegcl  20862  lspprvacl  20905  ellspsni  20907  lspsn  20908  lmhmplusg  20951  lmhmima  20954  lmhmpreima  20955  reslmhm  20959  lbsind2  20988  lsmcl  20990  lsmelval2  20992  lsppreli  20997  lspprabs  21002  pj1lmhm  21007  lssvs0or  21020  lspabs3  21031  lspfixed  21038  lspexch  21039  lsmcv  21051  lspsolv  21053  drngnidl  21153  rhmpreimaidl  21187  rngqiprngimfo  21211  rngqiprngfulem4  21224  gzrngunit  21350  zringlpirlem3  21374  prmirredlem  21382  znf1o  21461  znunithash  21474  freshmansdream  21484  frlmsubgval  21674  frlmvplusgvalc  21676  frlmvscaval  21677  frlmphllem  21689  frlmphl  21690  frlmssuvc1  21703  frlmsslsp  21705  frlmup1  21707  frlmup2  21708  lindfind2  21727  lindfrn  21730  f1lindf  21731  islindf4  21747  mplbas2  21949  evlslem3  21987  evlslem1  21989  coe1addfv  22151  lply1binom  22197  evl1addd  22228  evl1subd  22229  evl1muld  22230  mamudi  22290  mamudir  22291  1marepvmarrepid  22462  mdetrlin  22489  smadiadetglem1  22558  smadiadetg  22560  cramerimplem1  22570  mat2pmatscmxcl  22627  m2pmfzgsumcl  22635  pmatcollpw  22668  pmatcollpwfi  22669  pmatcollpw3fi1lem1  22673  cpmidpmatlem2  22758  cpmadugsumlemF  22763  chcoeffeqlem  22772  ntrin  22948  topssnei  23011  restbas  23045  restntr  23069  cnntri  23158  fiuncmp  23291  nllyrest  23373  nllyidm  23376  hausllycmp  23381  cldllycmp  23382  hauspwdom  23388  txcld  23490  txcn  23513  txlly  23523  txnlly  23524  txhaus  23534  txlm  23535  txkgen  23539  xkococnlem  23546  cnmpt2res  23564  xkoinjcn  23574  basqtop  23598  qtopeu  23603  trfbas2  23730  neifil  23767  hausflim  23868  alexsubALTlem2  23935  cnextfval  23949  cnextfvval  23952  cnextf  23953  cnextfres  23956  clssubg  23996  utop2nei  24138  utop3cls  24139  utopreg  24140  psmetlecl  24203  xmetlecl  24234  prdsxmetlem  24256  bldisj  24286  imasf1obl  24376  prdsbl  24379  stdbdmet  24404  stdbdmopn  24406  met2ndci  24410  metcnp  24429  metustto  24441  metustexhalf  24444  cfilucfil  24447  metucn  24459  lssnlm  24589  nmotri  24627  nmoid  24630  tgioo  24684  blcvx  24686  xrsmopn  24701  reperflem  24707  reconnlem2  24716  opnreen  24720  metdsge  24738  metdsre  24742  metdscnlem  24744  metnrmlem1a  24747  metnrmlem1  24748  metnrmlem3  24750  cncfmet  24802  cnmpopc  24822  icopnfcnv  24840  icopnfhmeo  24841  cnllycmp  24855  evth  24858  lebnumii  24865  nmoleub2lem3  25015  iscfil2  25166  cfil3i  25169  iscfil3  25173  cfilfcls  25174  iscau3  25178  iscmet3lem2  25192  caubl  25208  lmcau  25213  cssbn  25275  rrxcph  25292  minveclem2  25326  pjthlem1  25337  pjthlem2  25338  ivthicc  25359  ovollecl  25384  ovolunlem1a  25397  ovolunnul  25401  ovoliunlem1  25403  ismbl2  25428  nulmbl2  25437  unmbl  25438  volun  25446  voliunlem2  25452  ioombl1lem2  25460  uniioombllem2a  25483  uniioombllem3  25486  uniioombllem4  25487  dyaddisjlem  25496  dyadmaxlem  25498  opnmbllem  25502  volsup2  25506  volcn  25507  ismbfd  25540  mbfi1fseqlem1  25616  mbfi1fseqlem5  25620  itg2lecl  25639  itg2monolem2  25652  itg2gt0  25661  itgspliticc  25738  ellimc3  25780  limcres  25787  dvfval  25798  dvres3  25814  dvres3a  25815  dvmptresicc  25817  dvnff  25825  dvnadd  25831  dvn2bss  25832  dvnres  25833  dvcmul  25847  dvcmulf  25848  dvmptres3  25860  dvmptres2  25866  dvmptntr  25875  dvexp3  25882  dvferm1lem  25888  dvlip  25898  dvlipcn  25899  dvlip2  25900  c1liplem1  25901  dvgt0lem1  25907  dvgt0lem2  25908  dvne0  25916  lhop1lem  25918  lhop2  25920  lhop  25921  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcvx  25925  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  ftc1lem6  25948  ftc1  25949  ftc2ditglem  25952  itgsubstlem  25955  itgpowd  25957  tdeglem4  25965  mdegaddle  25979  mdegmullem  25983  ply1rem  26071  fta1glem2  26074  fta1blem  26076  ig1peu  26080  ig1pdvds  26085  dgrmulc  26177  dgrcolem1  26179  plydivlem4  26204  plydiveu  26206  fta1lem  26215  vieta1lem1  26218  vieta1lem2  26219  plyexmo  26221  taylfvallem1  26264  taylfval  26266  tayl0  26269  taylplem1  26270  taylply2  26275  taylply2OLD  26276  taylply  26277  dvtaylp  26278  dvntaylp  26279  dvntaylp0  26280  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmcaulem  26303  ulmcau  26304  ulmcn  26308  ulmdvlem1  26309  radcnvlem1  26322  radcnvle  26329  psercn  26336  pserdvlem2  26338  pserdv  26339  abelth  26351  tanregt0  26448  dvlog2lem  26561  efopn  26567  logtayllem  26568  logccv  26572  cxplt3  26609  cxpmul2zd  26625  cxpltd  26628  cxpled  26629  cxplt3d  26644  cxple3d  26645  dvsqrt  26651  cxpcn3  26658  cxpaddle  26662  cxpeq  26667  angcan  26712  angvald  26714  ang180lem2  26720  ang180  26724  isosctrlem3  26730  dquartlem1  26761  atantayl2  26848  leibpi  26852  log2tlbnd  26855  birthdaylem3  26863  xrlimcnp  26878  efrlim  26879  efrlimOLD  26880  o1cxp  26885  jensenlem2  26898  jensen  26899  fsumharmonic  26922  lgamucov  26948  lgamcvg2  26965  wilthlem1  26978  basellem3  26993  basellem6  26996  basellem8  26998  ppisval  27014  chtwordi  27066  ppiwordi  27072  mumullem2  27090  mpodvdsmulf1o  27104  dvdsmulf1o  27106  fsumvma  27124  fsumvma2  27125  chpchtsum  27130  chpub  27131  logfacubnd  27132  dchrmulcl  27160  dchrinv  27172  dchrptlem1  27175  dchrptlem2  27176  sumdchr2  27181  dchr2sum  27184  bposlem7  27201  lgslem1  27208  lgslem3  27210  lgsdirprm  27242  lgsqrlem2  27258  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem4  27289  lgseisen  27290  lgsquadlem1  27291  lgsquad2lem1  27295  lgsquad3  27298  m1lgs  27299  2sqlem7  27335  2sq2  27344  2sqmod  27347  chebbnd1lem2  27381  chebbnd1lem3  27382  rplogsumlem1  27395  rpvmasumlem  27398  dchrvmasumlem1  27406  dchrvmasum2lem  27407  dchrvmasumlema  27411  dchrisum0flblem2  27420  dchrisum0fno1  27422  dchrisum0re  27424  logdivsum  27444  pntrsumbnd2  27478  pntpbnd1a  27496  pntpbnd1  27497  pntibndlem2  27502  pntlemr  27513  pntlemj  27514  pntlemf  27516  pnt2  27524  padicabv  27541  ostth2lem2  27545  sltrec  27732  madebday  27811  sltn0  27817  addsproplem6  27881  sleadd1  27896  negsproplem6  27939  mulsproplem13  28031  mulsproplem14  28032  sltmuld  28040  mulsgt0d  28048  onscutlt  28165  n0sfincut  28246  halfcut  28333  f1otrg  28798  brbtwn2  28832  colinearalglem2  28834  axcgrtr  28842  axcgrid  28843  axsegconlem7  28850  axsegcon  28854  ax5seglem3  28858  ax5seglem6  28861  ax5seg  28865  axpaschlem  28867  axlowdimlem17  28885  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  ecgrtg  28910  usgredg2v  29154  vtxdgoddnumeven  29481  2trlond  29869  eupthp1  30145  nmobndi  30704  ubthlem2  30800  ubthlem3  30801  minvecolem2  30804  shuni  31229  pjhthlem1  31320  chscllem2  31567  pjcompi  31601  mayete3i  31657  unoplin  31849  hmoplin  31871  nmophmi  31960  mdslmd4i  32262  isoun  32625  submuladdd  32663  receqid  32668  xrge0addcld  32685  xrofsup  32690  eliccelico  32700  elicoelioo  32701  difioo  32705  hashpss  32734  sgnmul  32760  rexdiv  32846  mgcmnt1d  32923  mgcmnt2d  32924  chnub  32938  xrge0addgt0  32958  omndadd2d  33022  omndadd2rd  33023  omndmul2  33026  cycpmcl  33073  cycpm2tr  33076  cyc3evpm  33107  cycpmconjslem2  33112  fldgensdrg  33264  ofldchr  33292  qusker  33320  eqgvscpbl  33321  ringlsmss1  33367  ringlsmss2  33368  lidlmcld  33390  intlidl  33391  lidlunitel  33394  elrspunidl  33399  idlinsubrg  33402  isprmidlc  33418  rhmpreimaprmidl  33422  qsidomlem1  33423  ssdifidllem  33427  mxidlmaxv  33439  mxidlprm  33441  ssmxidllem  33444  opprmxidlabs  33458  qsdrnglem2  33467  resssra  33583  ply1degltdimlem  33618  lindsunlem  33620  sdrgfldext  33646  fldsdrgfldext  33657  finexttrb  33660  fldgenfldext  33663  fldextrspunlem1  33670  algextdeglem4  33710  algextdeglem8  33714  constrextdg2lem  33738  mdetpmtr2  33814  mdetpmtr12  33815  madjusmdetlem1  33817  madjusmdetlem4  33820  rhmpreimacn  33875  unitdivcld  33891  xrge0mulc1cn  33931  qqhnm  33980  esumcst  34053  esumfsup  34060  esumpmono  34069  esumcvg  34076  difelsiga  34123  sigapisys  34145  sigapildsys  34152  ldgenpisyslem1  34153  1stmbfm  34251  2ndmbfm  34252  dya2icoseg  34268  sibfinima  34330  probmeasb  34421  orvcgteel  34459  orvclteel  34464  ballotlemsima  34507  ballotlemfrceq  34520  ccatmulgnn0dir  34533  fct2relem  34588  ftc2re  34589  chtvalz  34620  subfacp1lem2a  35167  subfaclim  35175  erdsze2lem2  35191  cvmliftlem2  35273  cvmliftlem10  35281  cvmliftlem13  35283  cvmliftiota  35288  cvmlift2lem9  35298  cvmlift2lem11  35300  cvmlift2lem12  35301  cvmliftphtlem  35304  cvmlift3lem6  35311  cvmlift3lem7  35312  cvmlift3lem9  35314  snmlff  35316  mrsubfval  35495  wzel  35812  wsuclem  35813  brsegle  36096  opnregcld  36318  weiunfrlem  36452  fin2so  37601  poimirlem17  37631  poimirlem23  37637  opnmbllem0  37650  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem  37665  itg2addnc  37668  itg2gt0cn  37669  ftc1cnnclem  37685  ftc1cnnc  37686  areacirclem5  37706  indexdom  37728  sstotbnd2  37768  isbnd3  37778  isbnd3b  37779  cntotbnd  37790  ismtyima  37797  heibor1lem  37803  heiborlem8  37812  rrncmslem  37826  reheibor  37833  lkrlsp  39095  lshpkrlem5  39107  ldualssvscl  39151  ldualssvsubcl  39152  llnmlplnN  39533  llncvrlpln  39552  pmapjat1  39847  pclfinN  39894  lautlt  40085  lauteq  40089  lautco  40091  ltrn11  40120  ltrnle  40123  ltrneq2  40142  cdlemednuN  40294  cdleme20k  40313  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme21c  40321  cdleme22e  40338  cdleme22eALTN  40339  cdlemefrs32fva  40394  cdlemg4g  40610  cdlemg18b  40673  cdlemg18c  40674  cdlemj3  40817  dia2dimlem5  41062  dvhopN  41110  cdlemm10N  41112  dihjatcclem4  41415  dochexmidlem2  41455  lclkrlem2o  41515  lcfrlem5  41540  lcfrlem6  41541  lcdlssvscl  41600  mapdpglem6  41672  mapdpglem9  41674  mapdpglem12  41677  mapdpglem14  41679  mapdindp0  41713  hdmaprnlem7N  41849  hdmaprnlem8N  41850  hdmaprnlem3eN  41852  hgmapvvlem3  41919  dvun  42347  addinvcom  42420  evlsaddval  42556  evlsmulval  42557  evladdval  42563  evlmulval  42564  mzpsubst  42736  eldioph2lem1  42748  eldioph2lem2  42749  eldioph2b  42751  diophin  42760  irrapxlem2  42811  irrapxlem4  42813  irrapxlem5  42814  pellexlem1  42817  pellexlem2  42818  pellexlem6  42822  elpell1qr2  42860  pell1qrgaplem  42861  pell1qrgap  42862  pellqrex  42867  pellfundex  42874  pellfund14  42886  rmspecsqrtnq  42894  rmxyadd  42910  congsub  42959  mzpcong  42961  congrep  42962  acongtr  42967  acongrep  42969  jm2.19lem1  42978  jm2.22  42984  jm2.23  42985  jm2.26lem3  42990  jm2.26  42991  jm2.27a  42994  fnwe2lem2  43040  aomclem6  43048  hbtlem2  43113  hbtlem4  43115  hbtlem5  43117  dgraa0p  43138  rngunsnply  43158  proot1hash  43184  nnoeomeqom  43301  cantnf2  43314  omabs2  43321  naddcnff  43351  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  expgrowth  44324  fpmd  45257  abslt2sqd  45356  ioondisj2  45491  ioondisj1  45492  eliocre  45507  ioossioobi  45515  iooiinicc  45540  iooiinioc  45554  lptioo2  45629  limcresiooub  45640  limsupequzlem  45720  xlimmnfvlem2  45831  xlimpnfvlem2  45835  cncfuni  45884  cncfiooicclem1  45891  cxpcncf2  45897  dvcnre  45914  dvresntr  45916  dvresioo  45919  dvbdfbdioolem1  45926  dvnmptdivc  45936  dvnxpaek  45940  itgsinexplem1  45952  itgcoscmulx  45967  itgiccshift  45978  itgperiod  45979  ovolsplit  45986  stoweidlem11  46009  stoweidlem26  46024  stoweidlem34  46032  stoweidlem36  46034  stoweidlem38  46036  stirlinglem5  46076  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem20  46125  fourierdlem58  46162  fourierdlem72  46176  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem79  46183  fourierdlem80  46184  fourierdlem87  46191  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem113  46217  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  etransclem46  46278  etransclem47  46279  rrndistlt  46288  rrnprjdstle  46299  ioorrnopnxrlem  46304  sge0ssre  46395  sge0seq  46444  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmvlelem1  46593  hoidifhspdmvle  46618  hoiqssbllem2  46621  ovolval5lem2  46651  iinhoiicc  46672  iunhoiioo  46674  vonioolem2  46679  vonicclem2  46682  issmflem  46725  submodlt  47351  iccpartdisj  47438  m1expevenALTV  47648  fpprel2  47742  tgoldbach  47818  opstrgric  47926  gpg3kgrtriex  48080  nn0eo  48517  fdivpm  48532  refdivpm  48533  elbigolo1  48546  logbpw2m1  48556  fllog2  48557  dignn0flhalflem1  48604  dignn0flhalflem2  48605  itsclinecirc0in  48764  2itscplem2  48768  itscnhlinecirc02plem1  48771  iccdisj2  48885