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  4835  fr2nr  5631  soltmin  6125  f1oprg  6862  f1prex  7276  fveqf1o  7294  weniso  7346  fr3nr  7764  suppofssd  8200  smogt  8379  smocdmdom  8380  oacomf1o  8575  en2prd  9060  enpr2dOLD  9062  difsnen  9065  undomOLD  9072  enfixsn  9093  domss2  9148  ssenen  9163  marypha1lem  9443  fisupcl  9480  ordtypelem3  9532  ordtypelem8  9537  oieu  9551  oismo  9552  wofib  9557  wemaplem2  9559  wemapso  9563  wemapso2lem  9564  unxpwdom2  9600  infdifsn  9669  oemapvali  9696  cantnflem1c  9699  cantnflem1  9701  cantnf  9705  cnfcom3  9716  r1ordg  9790  dif1card  10022  infxpenlem  10025  dfac8clem  10044  infxp  10226  infmap2  10229  cflim2  10275  coftr  10285  fin2i2  10330  enfin2i  10333  fin23lem26  10337  fin23lem27  10340  fin23lem40  10363  isf32lem2  10366  isf32lem3  10367  isf32lem4  10368  isf32lem7  10371  isf32lem9  10373  fin1a2lem13  10424  fin12  10425  alephexp1  10591  gchdomtri  10641  fpwwe2lem11  10653  fpwwe2lem12  10654  gchpwdom  10682  gchhar  10691  adderpqlem  10966  mulerpqlem  10967  addassnq  10970  mulassnq  10971  distrnq  10973  mulidnq  10975  recmulnq  10976  ltexnq  10987  distrlem1pr  11037  distrlem4pr  11038  prlem936  11059  reclem3pr  11061  mulcmpblnr  11083  mulgt0d  11388  mul4d  11445  add4d  11462  add42d  11463  subcan  11536  addsub4d  11639  subadd4d  11640  sub4d  11641  2addsubd  11642  addsubeq4d  11643  muladdd  11693  mulsubd  11694  addgegt0d  11808  addgtge0d  11809  addge0d  11811  mulge0d  11812  le2subd  11855  ltleaddd  11856  leltaddd  11857  lt2subd  11859  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  12110  recreclt  12139  divgt0d  12175  mulgt1d  12176  lemulge11d  12177  lemulge12d  12178  ltmul12ad  12181  lemul12ad  12182  lemul12bd  12183  supmul1  12209  nndivtr  12285  qreccl  12983  ledivdivd  13074  lediv12ad  13108  lt2mul2divd  13118  xlt2add  13274  supxrun  13330  supxrre  13341  infxrre  13351  elicore  13413  iccss2  13432  iccssico2  13435  icossico2d  13436  lincmb01cmp  13510  iccf1o  13511  fzrev2i  13604  2tnp1ge0ge0  13844  m1modnnsub1  13933  modaddmodup  13950  modaddmodlo  13951  modsubdir  13956  fzennn  13984  sermono  14050  mulexpz  14118  expaddz  14122  sqdiv  14137  expsubd  14173  ltexp2a  14182  expmordi  14183  leexp2a  14188  expmulnbnd  14251  digit1  14253  lt2sqd  14272  le2sqd  14273  sq11d  14274  bcm1k  14331  bcp1n  14332  bcp1nk  14333  hashf1lem1  14471  cshw1  14838  2swrd2eqwrdeq  14970  ofccat  14986  absrele  15325  sqreulem  15376  sqrtmuld  15441  sqrtsq2d  15442  sqrtled  15443  sqrtltd  15444  sqr11d  15445  abs3lemd  15478  rlimuni  15564  climuni  15566  lo1resb  15578  o1resb  15580  2clim  15586  addcn2  15608  mulcn2  15610  o1of2  15627  o1rlimmul  15633  lo1add  15641  lo1mul  15642  isercolllem1  15679  caucvgrlem  15687  iseraltlem2  15697  iseraltlem3  15698  mptfzshft  15792  fsumrev  15793  fsum0diag2  15797  binomlem  15843  climcndslem1  15863  climcndslem2  15864  harmonic  15873  mertenslem1  15898  fprodser  15963  fprodrev  15991  efcllem  16091  moddvds  16281  dvds1  16336  dvdsext  16338  evennn2n  16368  bitsinv1  16459  sadaddlem  16483  sadasslem  16487  sadeq  16489  mulgcd  16565  dvdssqlem  16583  lcmftp  16653  rpmulgcd2  16673  coprmproddvdslem  16679  isprm5  16724  isprm6  16731  crth  16795  eulerthlem2  16799  prmdiveq  16803  pythagtriplem11  16843  pythagtriplem13  16845  pcgcd1  16895  pcprmpw2  16900  pcaddlem  16906  fldivp1  16915  4sqlem12  16974  4sqlem14  16976  4sqlem15  16977  4sqlem16  16978  vdwapun  16992  mreexexlem4d  17657  acsfn1  17671  acsfn2  17673  sscpwex  17826  rescabs  17844  yonedainv  18291  subm0  18791  pmtrfb  19444  psgnunilem1  19472  odmodnn0  19519  odeq  19529  dfod2  19543  sylow1lem1  19577  lsmsubg  19633  lsmmod  19654  lsmdisj2  19661  ghmplusg  19825  odadd  19829  gexexlem  19831  lt6abl  19874  cyggex2  19876  dprdfinv  20000  dmdprdsplitlem  20018  dpjidcl  20039  ablfacrp  20047  ablfacrp2  20048  ablfac1c  20052  ablfac1eu  20054  acsfn1p  20757  lcomfsupp  20857  lssvancl1  20900  lssvnegcl  20911  lspprvacl  20954  ellspsni  20956  lspsn  20957  lmhmplusg  21000  lmhmima  21003  lmhmpreima  21004  reslmhm  21008  lbsind2  21037  lsmcl  21039  lsmelval2  21041  lsppreli  21046  lspprabs  21051  pj1lmhm  21056  lssvs0or  21069  lspabs3  21080  lspfixed  21087  lspexch  21088  lsmcv  21100  lspsolv  21102  drngnidl  21202  rhmpreimaidl  21236  rngqiprngimfo  21260  rngqiprngfulem4  21273  gzrngunit  21399  zringlpirlem3  21423  prmirredlem  21431  znf1o  21510  znunithash  21523  freshmansdream  21533  frlmsubgval  21723  frlmvplusgvalc  21725  frlmvscaval  21726  frlmphllem  21738  frlmphl  21739  frlmssuvc1  21752  frlmsslsp  21754  frlmup1  21756  frlmup2  21757  lindfind2  21776  lindfrn  21779  f1lindf  21780  islindf4  21796  mplbas2  21998  evlslem3  22036  evlslem1  22038  coe1addfv  22200  lply1binom  22246  evl1addd  22277  evl1subd  22278  evl1muld  22279  mamudi  22339  mamudir  22340  1marepvmarrepid  22511  mdetrlin  22538  smadiadetglem1  22607  smadiadetg  22609  cramerimplem1  22619  mat2pmatscmxcl  22676  m2pmfzgsumcl  22684  pmatcollpw  22717  pmatcollpwfi  22718  pmatcollpw3fi1lem1  22722  cpmidpmatlem2  22807  cpmadugsumlemF  22812  chcoeffeqlem  22821  ntrin  22997  topssnei  23060  restbas  23094  restntr  23118  cnntri  23207  fiuncmp  23340  nllyrest  23422  nllyidm  23425  hausllycmp  23430  cldllycmp  23431  hauspwdom  23437  txcld  23539  txcn  23562  txlly  23572  txnlly  23573  txhaus  23583  txlm  23584  txkgen  23588  xkococnlem  23595  cnmpt2res  23613  xkoinjcn  23623  basqtop  23647  qtopeu  23652  trfbas2  23779  neifil  23816  hausflim  23917  alexsubALTlem2  23984  cnextfval  23998  cnextfvval  24001  cnextf  24002  cnextfres  24005  clssubg  24045  utop2nei  24187  utop3cls  24188  utopreg  24189  psmetlecl  24252  xmetlecl  24283  prdsxmetlem  24305  bldisj  24335  imasf1obl  24425  prdsbl  24428  stdbdmet  24453  stdbdmopn  24455  met2ndci  24459  metcnp  24478  metustto  24490  metustexhalf  24493  cfilucfil  24496  metucn  24508  lssnlm  24638  nmotri  24676  nmoid  24679  tgioo  24733  blcvx  24735  xrsmopn  24750  reperflem  24756  reconnlem2  24765  opnreen  24769  metdsge  24787  metdsre  24791  metdscnlem  24793  metnrmlem1a  24796  metnrmlem1  24797  metnrmlem3  24799  cncfmet  24851  cnmpopc  24871  icopnfcnv  24889  icopnfhmeo  24890  cnllycmp  24904  evth  24907  lebnumii  24914  nmoleub2lem3  25064  iscfil2  25216  cfil3i  25219  iscfil3  25223  cfilfcls  25224  iscau3  25228  iscmet3lem2  25242  caubl  25258  lmcau  25263  cssbn  25325  rrxcph  25342  minveclem2  25376  pjthlem1  25387  pjthlem2  25388  ivthicc  25409  ovollecl  25434  ovolunlem1a  25447  ovolunnul  25451  ovoliunlem1  25453  ismbl2  25478  nulmbl2  25487  unmbl  25488  volun  25496  voliunlem2  25502  ioombl1lem2  25510  uniioombllem2a  25533  uniioombllem3  25536  uniioombllem4  25537  dyaddisjlem  25546  dyadmaxlem  25548  opnmbllem  25552  volsup2  25556  volcn  25557  ismbfd  25590  mbfi1fseqlem1  25666  mbfi1fseqlem5  25670  itg2lecl  25689  itg2monolem2  25702  itg2gt0  25711  itgspliticc  25788  ellimc3  25830  limcres  25837  dvfval  25848  dvres3  25864  dvres3a  25865  dvmptresicc  25867  dvnff  25875  dvnadd  25881  dvn2bss  25882  dvnres  25883  dvcmul  25897  dvcmulf  25898  dvmptres3  25910  dvmptres2  25916  dvmptntr  25925  dvexp3  25932  dvferm1lem  25938  dvlip  25948  dvlipcn  25949  dvlip2  25950  c1liplem1  25951  dvgt0lem1  25957  dvgt0lem2  25958  dvne0  25966  lhop1lem  25968  lhop2  25970  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcvx  25975  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  ftc1lem6  25998  ftc1  25999  ftc2ditglem  26002  itgsubstlem  26005  itgpowd  26007  tdeglem4  26015  mdegaddle  26029  mdegmullem  26033  ply1rem  26121  fta1glem2  26124  fta1blem  26126  ig1peu  26130  ig1pdvds  26135  dgrmulc  26227  dgrcolem1  26229  plydivlem4  26254  plydiveu  26256  fta1lem  26265  vieta1lem1  26268  vieta1lem2  26269  plyexmo  26271  taylfvallem1  26314  taylfval  26316  tayl0  26319  taylplem1  26320  taylply2  26325  taylply2OLD  26326  taylply  26327  dvtaylp  26328  dvntaylp  26329  dvntaylp0  26330  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmcaulem  26353  ulmcau  26354  ulmcn  26358  ulmdvlem1  26359  radcnvlem1  26372  radcnvle  26379  psercn  26386  pserdvlem2  26388  pserdv  26389  abelth  26401  tanregt0  26498  dvlog2lem  26611  efopn  26617  logtayllem  26618  logccv  26622  cxplt3  26659  cxpmul2zd  26675  cxpltd  26678  cxpled  26679  cxplt3d  26694  cxple3d  26695  dvsqrt  26701  cxpcn3  26708  cxpaddle  26712  cxpeq  26717  angcan  26762  angvald  26764  ang180lem2  26770  ang180  26774  isosctrlem3  26780  dquartlem1  26811  atantayl2  26898  leibpi  26902  log2tlbnd  26905  birthdaylem3  26913  xrlimcnp  26928  efrlim  26929  efrlimOLD  26930  o1cxp  26935  jensenlem2  26948  jensen  26949  fsumharmonic  26972  lgamucov  26998  lgamcvg2  27015  wilthlem1  27028  basellem3  27043  basellem6  27046  basellem8  27048  ppisval  27064  chtwordi  27116  ppiwordi  27122  mumullem2  27140  mpodvdsmulf1o  27154  dvdsmulf1o  27156  fsumvma  27174  fsumvma2  27175  chpchtsum  27180  chpub  27181  logfacubnd  27182  dchrmulcl  27210  dchrinv  27222  dchrptlem1  27225  dchrptlem2  27226  sumdchr2  27231  dchr2sum  27234  bposlem7  27251  lgslem1  27258  lgslem3  27260  lgsdirprm  27292  lgsqrlem2  27308  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem4  27339  lgseisen  27340  lgsquadlem1  27341  lgsquad2lem1  27345  lgsquad3  27348  m1lgs  27349  2sqlem7  27385  2sq2  27394  2sqmod  27397  chebbnd1lem2  27431  chebbnd1lem3  27432  rplogsumlem1  27445  rpvmasumlem  27448  dchrvmasumlem1  27456  dchrvmasum2lem  27457  dchrvmasumlema  27461  dchrisum0flblem2  27470  dchrisum0fno1  27472  dchrisum0re  27474  logdivsum  27494  pntrsumbnd2  27528  pntpbnd1a  27546  pntpbnd1  27547  pntibndlem2  27552  pntlemr  27563  pntlemj  27564  pntlemf  27566  pnt2  27574  padicabv  27591  ostth2lem2  27595  sltrec  27782  madebday  27855  sltn0  27860  addsproplem6  27924  sleadd1  27939  negsproplem6  27982  mulsproplem13  28071  mulsproplem14  28072  sltmuld  28080  mulsgt0d  28088  halfcut  28333  f1otrg  28796  brbtwn2  28830  colinearalglem2  28832  axcgrtr  28840  axcgrid  28841  axsegconlem7  28848  axsegcon  28852  ax5seglem3  28856  ax5seglem6  28859  ax5seg  28863  axpaschlem  28865  axlowdimlem17  28883  axcontlem2  28890  axcontlem4  28892  axcontlem7  28895  axcontlem8  28896  ecgrtg  28908  usgredg2v  29152  vtxdgoddnumeven  29479  2trlond  29867  eupthp1  30143  nmobndi  30702  ubthlem2  30798  ubthlem3  30799  minvecolem2  30802  shuni  31227  pjhthlem1  31318  chscllem2  31565  pjcompi  31599  mayete3i  31655  unoplin  31847  hmoplin  31869  nmophmi  31958  mdslmd4i  32260  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  33254  ofldchr  33282  qusker  33310  eqgvscpbl  33311  ringlsmss1  33357  ringlsmss2  33358  lidlmcld  33380  intlidl  33381  lidlunitel  33384  elrspunidl  33389  idlinsubrg  33392  isprmidlc  33408  rhmpreimaprmidl  33412  qsidomlem1  33413  ssdifidllem  33417  mxidlmaxv  33429  mxidlprm  33431  ssmxidllem  33434  opprmxidlabs  33448  qsdrnglem2  33457  resssra  33573  ply1degltdimlem  33608  lindsunlem  33610  sdrgfldext  33638  fldsdrgfldext  33649  finexttrb  33652  fldgenfldext  33655  fldextrspunlem1  33662  algextdeglem4  33700  algextdeglem8  33704  constrextdg2lem  33728  mdetpmtr2  33801  mdetpmtr12  33802  madjusmdetlem1  33804  madjusmdetlem4  33807  rhmpreimacn  33862  unitdivcld  33878  xrge0mulc1cn  33918  qqhnm  33967  esumcst  34040  esumfsup  34047  esumpmono  34056  esumcvg  34063  difelsiga  34110  sigapisys  34132  sigapildsys  34139  ldgenpisyslem1  34140  1stmbfm  34238  2ndmbfm  34239  dya2icoseg  34255  sibfinima  34317  probmeasb  34408  orvcgteel  34446  orvclteel  34451  ballotlemsima  34494  ballotlemfrceq  34507  ccatmulgnn0dir  34520  fct2relem  34575  ftc2re  34576  chtvalz  34607  subfacp1lem2a  35148  subfaclim  35156  erdsze2lem2  35172  cvmliftlem2  35254  cvmliftlem10  35262  cvmliftlem13  35264  cvmliftiota  35269  cvmlift2lem9  35279  cvmlift2lem11  35281  cvmlift2lem12  35282  cvmliftphtlem  35285  cvmlift3lem6  35292  cvmlift3lem7  35293  cvmlift3lem9  35295  snmlff  35297  mrsubfval  35476  wzel  35788  wsuclem  35789  brsegle  36072  opnregcld  36294  weiunfrlem  36428  fin2so  37577  poimirlem17  37607  poimirlem23  37613  opnmbllem0  37626  mblfinlem3  37629  mblfinlem4  37630  itg2addnclem  37641  itg2addnc  37644  itg2gt0cn  37645  ftc1cnnclem  37661  ftc1cnnc  37662  areacirclem5  37682  indexdom  37704  sstotbnd2  37744  isbnd3  37754  isbnd3b  37755  cntotbnd  37766  ismtyima  37773  heibor1lem  37779  heiborlem8  37788  rrncmslem  37802  reheibor  37809  lkrlsp  39066  lshpkrlem5  39078  ldualssvscl  39122  ldualssvsubcl  39123  llnmlplnN  39504  llncvrlpln  39523  pmapjat1  39818  pclfinN  39865  lautlt  40056  lauteq  40060  lautco  40062  ltrn11  40091  ltrnle  40094  ltrneq2  40113  cdlemednuN  40265  cdleme20k  40284  cdleme20l2  40286  cdleme20l  40287  cdleme20m  40288  cdleme21c  40292  cdleme22e  40309  cdleme22eALTN  40310  cdlemefrs32fva  40365  cdlemg4g  40581  cdlemg18b  40644  cdlemg18c  40645  cdlemj3  40788  dia2dimlem5  41033  dvhopN  41081  cdlemm10N  41083  dihjatcclem4  41386  dochexmidlem2  41426  lclkrlem2o  41486  lcfrlem5  41511  lcfrlem6  41512  lcdlssvscl  41571  mapdpglem6  41643  mapdpglem9  41645  mapdpglem12  41648  mapdpglem14  41650  mapdindp0  41684  hdmaprnlem7N  41820  hdmaprnlem8N  41821  hdmaprnlem3eN  41823  hgmapvvlem3  41890  dvun  42349  addinvcom  42421  evlsaddval  42538  evlsmulval  42539  evladdval  42545  evlmulval  42546  mzpsubst  42718  eldioph2lem1  42730  eldioph2lem2  42731  eldioph2b  42733  diophin  42742  irrapxlem2  42793  irrapxlem4  42795  irrapxlem5  42796  pellexlem1  42799  pellexlem2  42800  pellexlem6  42804  elpell1qr2  42842  pell1qrgaplem  42843  pell1qrgap  42844  pellqrex  42849  pellfundex  42856  pellfund14  42868  rmspecsqrtnq  42876  rmxyadd  42892  congsub  42941  mzpcong  42943  congrep  42944  acongtr  42949  acongrep  42951  jm2.19lem1  42960  jm2.22  42966  jm2.23  42967  jm2.26lem3  42972  jm2.26  42973  jm2.27a  42976  fnwe2lem2  43022  aomclem6  43030  hbtlem2  43095  hbtlem4  43097  hbtlem5  43099  dgraa0p  43120  rngunsnply  43140  proot1hash  43166  nnoeomeqom  43283  cantnf2  43296  omabs2  43303  naddcnff  43333  naddcnffo  43335  naddcnfcom  43337  naddcnfid1  43338  expgrowth  44307  fpmd  45235  abslt2sqd  45335  ioondisj2  45470  ioondisj1  45471  eliocre  45486  ioossioobi  45494  iooiinicc  45519  iooiinioc  45533  lptioo2  45608  limcresiooub  45619  limsupequzlem  45699  xlimmnfvlem2  45810  xlimpnfvlem2  45814  cncfuni  45863  cncfiooicclem1  45870  cxpcncf2  45876  dvcnre  45893  dvresntr  45895  dvresioo  45898  dvbdfbdioolem1  45905  dvnmptdivc  45915  dvnxpaek  45919  itgsinexplem1  45931  itgcoscmulx  45946  itgiccshift  45957  itgperiod  45958  ovolsplit  45965  stoweidlem11  45988  stoweidlem26  46003  stoweidlem34  46011  stoweidlem36  46013  stoweidlem38  46015  stirlinglem5  46055  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem20  46104  fourierdlem58  46141  fourierdlem72  46155  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem79  46162  fourierdlem80  46163  fourierdlem87  46170  fourierdlem94  46177  fourierdlem103  46186  fourierdlem104  46187  fourierdlem107  46190  fourierdlem113  46196  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  etransclem46  46257  etransclem47  46258  rrndistlt  46267  rrnprjdstle  46278  ioorrnopnxrlem  46283  sge0ssre  46374  sge0seq  46423  hsphoidmvle2  46562  hsphoidmvle  46563  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmvlelem1  46572  hoidifhspdmvle  46597  hoiqssbllem2  46600  ovolval5lem2  46630  iinhoiicc  46651  iunhoiioo  46653  vonioolem2  46658  vonicclem2  46661  issmflem  46704  submodlt  47327  iccpartdisj  47399  m1expevenALTV  47609  fpprel2  47703  tgoldbach  47779  opstrgric  47887  gpg3kgrtriex  48039  nn0eo  48456  fdivpm  48471  refdivpm  48472  elbigolo1  48485  logbpw2m1  48495  fllog2  48496  dignn0flhalflem1  48543  dignn0flhalflem2  48544  itsclinecirc0in  48703  2itscplem2  48707  itscnhlinecirc02plem1  48710  iccdisj2  48819