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  4811  fr2nr  5593  soltmin  6083  f1oprg  6808  f1prex  7218  fveqf1o  7236  weniso  7288  fr3nr  7705  suppofssd  8133  smogt  8287  smocdmdom  8288  oacomf1o  8480  en2prd  8969  difsnen  8972  enfixsn  8999  domss2  9049  ssenen  9064  marypha1lem  9317  fisupcl  9354  ordtypelem3  9406  ordtypelem8  9411  oieu  9425  oismo  9426  wofib  9431  wemaplem2  9433  wemapso  9437  wemapso2lem  9438  unxpwdom2  9474  infdifsn  9547  oemapvali  9574  cantnflem1c  9577  cantnflem1  9579  cantnf  9583  cnfcom3  9594  r1ordg  9668  dif1card  9898  infxpenlem  9901  dfac8clem  9920  infxp  10102  infmap2  10105  cflim2  10151  coftr  10161  fin2i2  10206  enfin2i  10209  fin23lem26  10213  fin23lem27  10216  fin23lem40  10239  isf32lem2  10242  isf32lem3  10243  isf32lem4  10244  isf32lem7  10247  isf32lem9  10249  fin1a2lem13  10300  fin12  10301  alephexp1  10467  gchdomtri  10517  fpwwe2lem11  10529  fpwwe2lem12  10530  gchpwdom  10558  gchhar  10567  adderpqlem  10842  mulerpqlem  10843  addassnq  10846  mulassnq  10847  distrnq  10849  mulidnq  10851  recmulnq  10852  ltexnq  10863  distrlem1pr  10913  distrlem4pr  10914  prlem936  10935  reclem3pr  10937  mulcmpblnr  10959  mulgt0d  11265  mul4d  11322  add4d  11339  add42d  11340  subcan  11413  addsub4d  11516  subadd4d  11517  sub4d  11518  2addsubd  11519  addsubeq4d  11520  muladdd  11572  mulsubd  11573  addgegt0d  11687  addgtge0d  11688  addge0d  11690  mulge0d  11691  le2subd  11734  ltleaddd  11735  leltaddd  11736  lt2subd  11738  divdivdiv  11819  divcan5  11820  divne0d  11910  recdivd  11911  recdiv2d  11912  divcan6d  11913  ddcand  11914  rec11d  11915  divmuldivd  11935  divmul13d  11936  divmul24d  11937  divadddivd  11938  divsubdivd  11939  divmuleqd  11940  divdivdivd  11941  mulge0b  11989  recreclt  12018  divgt0d  12054  mulgt1d  12055  lemulge11d  12056  lemulge12d  12057  ltmul12ad  12060  lemul12ad  12061  lemul12bd  12062  supmul1  12088  nndivtr  12169  qreccl  12864  ledivdivd  12956  lediv12ad  12990  lt2mul2divd  13000  xlt2add  13156  supxrun  13212  supxrre  13223  infxrre  13233  elicore  13295  iccss2  13314  iccssico2  13317  icossico2d  13318  lincmb01cmp  13392  iccf1o  13393  fzrev2i  13486  2tnp1ge0ge0  13730  m1modnnsub1  13821  modaddmodup  13838  modaddmodlo  13839  modsubdir  13844  fzennn  13872  sermono  13938  mulexpz  14006  expaddz  14010  sqdiv  14025  expsubd  14061  ltexp2a  14070  expmordi  14071  leexp2a  14076  expmulnbnd  14139  digit1  14141  lt2sqd  14160  le2sqd  14161  sq11d  14162  bcm1k  14219  bcp1n  14220  bcp1nk  14221  hashf1lem1  14359  cshw1  14726  2swrd2eqwrdeq  14857  ofccat  14873  absrele  15212  sqreulem  15264  sqrtmuld  15329  sqrtsq2d  15330  sqrtled  15331  sqrtltd  15332  sqr11d  15333  abs3lemd  15368  rlimuni  15454  climuni  15456  lo1resb  15468  o1resb  15470  2clim  15476  addcn2  15498  mulcn2  15500  o1of2  15517  o1rlimmul  15523  lo1add  15531  lo1mul  15532  isercolllem1  15569  caucvgrlem  15577  iseraltlem2  15587  iseraltlem3  15588  mptfzshft  15682  fsumrev  15683  fsum0diag2  15687  binomlem  15733  climcndslem1  15753  climcndslem2  15754  harmonic  15763  mertenslem1  15788  fprodser  15853  fprodrev  15881  efcllem  15981  moddvds  16171  dvds1  16227  dvdsext  16229  evennn2n  16259  bitsinv1  16350  sadaddlem  16374  sadasslem  16378  sadeq  16380  mulgcd  16456  dvdssqlem  16474  lcmftp  16544  rpmulgcd2  16564  coprmproddvdslem  16570  isprm5  16615  isprm6  16622  crth  16686  eulerthlem2  16690  prmdiveq  16694  pythagtriplem11  16734  pythagtriplem13  16736  pcgcd1  16786  pcprmpw2  16791  pcaddlem  16797  fldivp1  16806  4sqlem12  16865  4sqlem14  16867  4sqlem15  16868  4sqlem16  16869  vdwapun  16883  mreexexlem4d  17550  acsfn1  17564  acsfn2  17566  sscpwex  17719  rescabs  17737  yonedainv  18184  chnub  18525  subm0  18720  pmtrfb  19375  psgnunilem1  19403  odmodnn0  19450  odeq  19460  dfod2  19474  sylow1lem1  19508  lsmsubg  19564  lsmmod  19585  lsmdisj2  19592  ghmplusg  19756  odadd  19760  gexexlem  19762  lt6abl  19805  cyggex2  19807  dprdfinv  19931  dmdprdsplitlem  19949  dpjidcl  19970  ablfacrp  19978  ablfacrp2  19979  ablfac1c  19983  ablfac1eu  19985  omndadd2d  20040  omndadd2rd  20041  omndmul2  20043  acsfn1p  20712  lcomfsupp  20833  lssvancl1  20876  lssvnegcl  20887  lspprvacl  20930  ellspsni  20932  lspsn  20933  lmhmplusg  20976  lmhmima  20979  lmhmpreima  20980  reslmhm  20984  lbsind2  21013  lsmcl  21015  lsmelval2  21017  lsppreli  21022  lspprabs  21027  pj1lmhm  21032  lssvs0or  21045  lspabs3  21056  lspfixed  21063  lspexch  21064  lsmcv  21076  lspsolv  21078  drngnidl  21178  rhmpreimaidl  21212  rngqiprngimfo  21236  rngqiprngfulem4  21249  gzrngunit  21368  zringlpirlem3  21399  prmirredlem  21407  znf1o  21486  znunithash  21499  freshmansdream  21509  ofldchr  21511  frlmsubgval  21700  frlmvplusgvalc  21702  frlmvscaval  21703  frlmphllem  21715  frlmphl  21716  frlmssuvc1  21729  frlmsslsp  21731  frlmup1  21733  frlmup2  21734  lindfind2  21753  lindfrn  21756  f1lindf  21757  islindf4  21773  mplbas2  21975  evlslem3  22013  evlslem1  22015  coe1addfv  22177  lply1binom  22223  evl1addd  22254  evl1subd  22255  evl1muld  22256  mamudi  22316  mamudir  22317  1marepvmarrepid  22488  mdetrlin  22515  smadiadetglem1  22584  smadiadetg  22586  cramerimplem1  22596  mat2pmatscmxcl  22653  m2pmfzgsumcl  22661  pmatcollpw  22694  pmatcollpwfi  22695  pmatcollpw3fi1lem1  22699  cpmidpmatlem2  22784  cpmadugsumlemF  22789  chcoeffeqlem  22798  ntrin  22974  topssnei  23037  restbas  23071  restntr  23095  cnntri  23184  fiuncmp  23317  nllyrest  23399  nllyidm  23402  hausllycmp  23407  cldllycmp  23408  hauspwdom  23414  txcld  23516  txcn  23539  txlly  23549  txnlly  23550  txhaus  23560  txlm  23561  txkgen  23565  xkococnlem  23572  cnmpt2res  23590  xkoinjcn  23600  basqtop  23624  qtopeu  23629  trfbas2  23756  neifil  23793  hausflim  23894  alexsubALTlem2  23961  cnextfval  23975  cnextfvval  23978  cnextf  23979  cnextfres  23982  clssubg  24022  utop2nei  24163  utop3cls  24164  utopreg  24165  psmetlecl  24228  xmetlecl  24259  prdsxmetlem  24281  bldisj  24311  imasf1obl  24401  prdsbl  24404  stdbdmet  24429  stdbdmopn  24431  met2ndci  24435  metcnp  24454  metustto  24466  metustexhalf  24469  cfilucfil  24472  metucn  24484  lssnlm  24614  nmotri  24652  nmoid  24655  tgioo  24709  blcvx  24711  xrsmopn  24726  reperflem  24732  reconnlem2  24741  opnreen  24745  metdsge  24763  metdsre  24767  metdscnlem  24769  metnrmlem1a  24772  metnrmlem1  24773  metnrmlem3  24775  cncfmet  24827  cnmpopc  24847  icopnfcnv  24865  icopnfhmeo  24866  cnllycmp  24880  evth  24883  lebnumii  24890  nmoleub2lem3  25040  iscfil2  25191  cfil3i  25194  iscfil3  25198  cfilfcls  25199  iscau3  25203  iscmet3lem2  25217  caubl  25233  lmcau  25238  cssbn  25300  rrxcph  25317  minveclem2  25351  pjthlem1  25362  pjthlem2  25363  ivthicc  25384  ovollecl  25409  ovolunlem1a  25422  ovolunnul  25426  ovoliunlem1  25428  ismbl2  25453  nulmbl2  25462  unmbl  25463  volun  25471  voliunlem2  25477  ioombl1lem2  25485  uniioombllem2a  25508  uniioombllem3  25511  uniioombllem4  25512  dyaddisjlem  25521  dyadmaxlem  25523  opnmbllem  25527  volsup2  25531  volcn  25532  ismbfd  25565  mbfi1fseqlem1  25641  mbfi1fseqlem5  25645  itg2lecl  25664  itg2monolem2  25677  itg2gt0  25686  itgspliticc  25763  ellimc3  25805  limcres  25812  dvfval  25823  dvres3  25839  dvres3a  25840  dvmptresicc  25842  dvnff  25850  dvnadd  25856  dvn2bss  25857  dvnres  25858  dvcmul  25872  dvcmulf  25873  dvmptres3  25885  dvmptres2  25891  dvmptntr  25900  dvexp3  25907  dvferm1lem  25913  dvlip  25923  dvlipcn  25924  dvlip2  25925  c1liplem1  25926  dvgt0lem1  25932  dvgt0lem2  25933  dvne0  25941  lhop1lem  25943  lhop2  25945  lhop  25946  dvcnvrelem1  25947  dvcnvrelem2  25948  dvcvx  25950  dvfsumle  25951  dvfsumleOLD  25952  dvfsumabs  25954  dvfsumlem2  25958  dvfsumlem2OLD  25959  ftc1lem6  25973  ftc1  25974  ftc2ditglem  25977  itgsubstlem  25980  itgpowd  25982  tdeglem4  25990  mdegaddle  26004  mdegmullem  26008  ply1rem  26096  fta1glem2  26099  fta1blem  26101  ig1peu  26105  ig1pdvds  26110  dgrmulc  26202  dgrcolem1  26204  plydivlem4  26229  plydiveu  26231  fta1lem  26240  vieta1lem1  26243  vieta1lem2  26244  plyexmo  26246  taylfvallem1  26289  taylfval  26291  tayl0  26294  taylplem1  26295  taylply2  26300  taylply2OLD  26301  taylply  26302  dvtaylp  26303  dvntaylp  26304  dvntaylp0  26305  taylthlem1  26306  taylthlem2  26307  taylthlem2OLD  26308  ulmcaulem  26328  ulmcau  26329  ulmcn  26333  ulmdvlem1  26334  radcnvlem1  26347  radcnvle  26354  psercn  26361  pserdvlem2  26363  pserdv  26364  abelth  26376  tanregt0  26473  dvlog2lem  26586  efopn  26592  logtayllem  26593  logccv  26597  cxplt3  26634  cxpmul2zd  26650  cxpltd  26653  cxpled  26654  cxplt3d  26669  cxple3d  26670  dvsqrt  26676  cxpcn3  26683  cxpaddle  26687  cxpeq  26692  angcan  26737  angvald  26739  ang180lem2  26745  ang180  26749  isosctrlem3  26755  dquartlem1  26786  atantayl2  26873  leibpi  26877  log2tlbnd  26880  birthdaylem3  26888  xrlimcnp  26903  efrlim  26904  efrlimOLD  26905  o1cxp  26910  jensenlem2  26923  jensen  26924  fsumharmonic  26947  lgamucov  26973  lgamcvg2  26990  wilthlem1  27003  basellem3  27018  basellem6  27021  basellem8  27023  ppisval  27039  chtwordi  27091  ppiwordi  27097  mumullem2  27115  mpodvdsmulf1o  27129  dvdsmulf1o  27131  fsumvma  27149  fsumvma2  27150  chpchtsum  27155  chpub  27156  logfacubnd  27157  dchrmulcl  27185  dchrinv  27197  dchrptlem1  27200  dchrptlem2  27201  sumdchr2  27206  dchr2sum  27209  bposlem7  27226  lgslem1  27233  lgslem3  27235  lgsdirprm  27267  lgsqrlem2  27283  lgseisenlem1  27311  lgseisenlem2  27312  lgseisenlem4  27314  lgseisen  27315  lgsquadlem1  27316  lgsquad2lem1  27320  lgsquad3  27323  m1lgs  27324  2sqlem7  27360  2sq2  27369  2sqmod  27372  chebbnd1lem2  27406  chebbnd1lem3  27407  rplogsumlem1  27420  rpvmasumlem  27423  dchrvmasumlem1  27431  dchrvmasum2lem  27432  dchrvmasumlema  27436  dchrisum0flblem2  27445  dchrisum0fno1  27447  dchrisum0re  27449  logdivsum  27469  pntrsumbnd2  27503  pntpbnd1a  27521  pntpbnd1  27522  pntibndlem2  27527  pntlemr  27538  pntlemj  27539  pntlemf  27541  pnt2  27549  padicabv  27566  ostth2lem2  27570  slerecd  27759  sltrecd  27761  madebday  27843  addsproplem6  27915  negsproplem6  27973  mulsproplem13  28065  mulsproplem14  28066  sltmuld  28074  mulsgt0d  28082  f1otrg  28847  brbtwn2  28881  colinearalglem2  28883  axcgrtr  28891  axcgrid  28892  axsegconlem7  28899  axsegcon  28903  ax5seglem3  28907  ax5seglem6  28910  ax5seg  28914  axpaschlem  28916  axlowdimlem17  28934  axcontlem2  28941  axcontlem4  28943  axcontlem7  28946  axcontlem8  28947  ecgrtg  28959  usgredg2v  29203  vtxdgoddnumeven  29530  2trlond  29915  eupthp1  30191  nmobndi  30750  ubthlem2  30846  ubthlem3  30847  minvecolem2  30850  shuni  31275  pjhthlem1  31366  chscllem2  31613  pjcompi  31647  mayete3i  31703  unoplin  31895  hmoplin  31917  nmophmi  32006  mdslmd4i  32308  isoun  32678  submuladdd  32718  receqid  32723  xrge0addcld  32740  xrofsup  32745  eliccelico  32755  elicoelioo  32756  difioo  32760  hashpss  32786  sgnmul  32813  rexdiv  32901  mgcmnt1d  32973  mgcmnt2d  32974  xrge0addgt0  32993  cycpmcl  33080  cycpm2tr  33083  cyc3evpm  33114  cycpmconjslem2  33119  fldgensdrg  33275  qusker  33309  eqgvscpbl  33310  ringlsmss1  33356  ringlsmss2  33357  lidlmcld  33379  intlidl  33380  lidlunitel  33383  elrspunidl  33388  idlinsubrg  33391  isprmidlc  33407  rhmpreimaprmidl  33411  qsidomlem1  33412  ssdifidllem  33416  mxidlmaxv  33428  mxidlprm  33430  ssmxidllem  33433  opprmxidlabs  33447  qsdrnglem2  33456  mplvrpmmhm  33571  mplvrpmrhm  33572  resssra  33594  ply1degltdimlem  33630  lindsunlem  33632  sdrgfldext  33658  fldsdrgfldext  33669  finexttrb  33673  fldgenfldext  33676  fldextrspunlem1  33683  algextdeglem4  33728  algextdeglem8  33732  constrextdg2lem  33756  mdetpmtr2  33832  mdetpmtr12  33833  madjusmdetlem1  33835  madjusmdetlem4  33838  rhmpreimacn  33893  unitdivcld  33909  xrge0mulc1cn  33949  qqhnm  33998  esumcst  34071  esumfsup  34078  esumpmono  34087  esumcvg  34094  difelsiga  34141  sigapisys  34163  sigapildsys  34170  ldgenpisyslem1  34171  1stmbfm  34268  2ndmbfm  34269  dya2icoseg  34285  sibfinima  34347  probmeasb  34438  orvcgteel  34476  orvclteel  34481  ballotlemsima  34524  ballotlemfrceq  34537  ccatmulgnn0dir  34550  fct2relem  34605  ftc2re  34606  chtvalz  34637  r1filimi  35106  subfacp1lem2a  35212  subfaclim  35220  erdsze2lem2  35236  cvmliftlem2  35318  cvmliftlem10  35326  cvmliftlem13  35328  cvmliftiota  35333  cvmlift2lem9  35343  cvmlift2lem11  35345  cvmlift2lem12  35346  cvmliftphtlem  35349  cvmlift3lem6  35356  cvmlift3lem7  35357  cvmlift3lem9  35359  snmlff  35361  mrsubfval  35540  wzel  35857  wsuclem  35858  brsegle  36141  opnregcld  36363  weiunfrlem  36497  fin2so  37646  poimirlem17  37676  poimirlem23  37682  opnmbllem0  37695  mblfinlem3  37698  mblfinlem4  37699  itg2addnclem  37710  itg2addnc  37713  itg2gt0cn  37714  ftc1cnnclem  37730  ftc1cnnc  37731  areacirclem5  37751  indexdom  37773  sstotbnd2  37813  isbnd3  37823  isbnd3b  37824  cntotbnd  37835  ismtyima  37842  heibor1lem  37848  heiborlem8  37857  rrncmslem  37871  reheibor  37878  lkrlsp  39140  lshpkrlem5  39152  ldualssvscl  39196  ldualssvsubcl  39197  llnmlplnN  39577  llncvrlpln  39596  pmapjat1  39891  pclfinN  39938  lautlt  40129  lauteq  40133  lautco  40135  ltrn11  40164  ltrnle  40167  ltrneq2  40186  cdlemednuN  40338  cdleme20k  40357  cdleme20l2  40359  cdleme20l  40360  cdleme20m  40361  cdleme21c  40365  cdleme22e  40382  cdleme22eALTN  40383  cdlemefrs32fva  40438  cdlemg4g  40654  cdlemg18b  40717  cdlemg18c  40718  cdlemj3  40861  dia2dimlem5  41106  dvhopN  41154  cdlemm10N  41156  dihjatcclem4  41459  dochexmidlem2  41499  lclkrlem2o  41559  lcfrlem5  41584  lcfrlem6  41585  lcdlssvscl  41644  mapdpglem6  41716  mapdpglem9  41718  mapdpglem12  41721  mapdpglem14  41723  mapdindp0  41757  hdmaprnlem7N  41893  hdmaprnlem8N  41894  hdmaprnlem3eN  41896  hgmapvvlem3  41963  dvun  42391  addinvcom  42464  evlsaddval  42600  evlsmulval  42601  evladdval  42607  evlmulval  42608  mzpsubst  42780  eldioph2lem1  42792  eldioph2lem2  42793  eldioph2b  42795  diophin  42804  irrapxlem2  42855  irrapxlem4  42857  irrapxlem5  42858  pellexlem1  42861  pellexlem2  42862  pellexlem6  42866  elpell1qr2  42904  pell1qrgaplem  42905  pell1qrgap  42906  pellqrex  42911  pellfundex  42918  pellfund14  42930  rmspecsqrtnq  42938  rmxyadd  42953  congsub  43002  mzpcong  43004  congrep  43005  acongtr  43010  acongrep  43012  jm2.19lem1  43021  jm2.22  43027  jm2.23  43028  jm2.26lem3  43033  jm2.26  43034  jm2.27a  43037  fnwe2lem2  43083  aomclem6  43091  hbtlem2  43156  hbtlem4  43158  hbtlem5  43160  dgraa0p  43181  rngunsnply  43201  proot1hash  43227  nnoeomeqom  43344  cantnf2  43357  omabs2  43364  naddcnff  43394  naddcnffo  43396  naddcnfcom  43398  naddcnfid1  43399  expgrowth  44367  fpmd  45299  abslt2sqd  45398  ioondisj2  45532  ioondisj1  45533  eliocre  45548  ioossioobi  45556  iooiinicc  45581  iooiinioc  45595  lptioo2  45670  limcresiooub  45679  limsupequzlem  45759  xlimmnfvlem2  45870  xlimpnfvlem2  45874  cncfuni  45923  cncfiooicclem1  45930  cxpcncf2  45936  dvcnre  45953  dvresntr  45955  dvresioo  45958  dvbdfbdioolem1  45965  dvnmptdivc  45975  dvnxpaek  45979  itgsinexplem1  45991  itgcoscmulx  46006  itgiccshift  46017  itgperiod  46018  ovolsplit  46025  stoweidlem11  46048  stoweidlem26  46063  stoweidlem34  46071  stoweidlem36  46073  stoweidlem38  46075  stirlinglem5  46115  dirkercncflem2  46141  dirkercncflem4  46143  fourierdlem20  46164  fourierdlem58  46201  fourierdlem72  46215  fourierdlem73  46216  fourierdlem74  46217  fourierdlem75  46218  fourierdlem76  46219  fourierdlem79  46222  fourierdlem80  46223  fourierdlem87  46230  fourierdlem94  46237  fourierdlem103  46246  fourierdlem104  46247  fourierdlem107  46250  fourierdlem113  46256  sqwvfoura  46265  sqwvfourb  46266  fourierswlem  46267  fouriersw  46268  etransclem46  46317  etransclem47  46318  rrndistlt  46327  rrnprjdstle  46338  ioorrnopnxrlem  46343  sge0ssre  46434  sge0seq  46483  hsphoidmvle2  46622  hsphoidmvle  46623  hoidmv1lelem1  46628  hoidmv1lelem2  46629  hoidmv1lelem3  46630  hoidmvlelem1  46632  hoidifhspdmvle  46657  hoiqssbllem2  46660  ovolval5lem2  46690  iinhoiicc  46711  iunhoiioo  46713  vonioolem2  46718  vonicclem2  46721  issmflem  46764  submodlt  47380  iccpartdisj  47467  m1expevenALTV  47677  fpprel2  47771  tgoldbach  47847  opstrgric  47956  gpg3kgrtriex  48119  nn0eo  48559  fdivpm  48574  refdivpm  48575  elbigolo1  48588  logbpw2m1  48598  fllog2  48599  dignn0flhalflem1  48646  dignn0flhalflem2  48647  itsclinecirc0in  48806  2itscplem2  48810  itscnhlinecirc02plem1  48813  iccdisj2  48927