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  4810  fr2nr  5596  soltmin  6088  f1oprg  6814  f1prex  7224  fveqf1o  7242  weniso  7294  fr3nr  7711  suppofssd  8139  smogt  8293  smocdmdom  8294  oacomf1o  8486  en2prd  8975  difsnen  8978  enfixsn  9005  domss2  9055  ssenen  9070  marypha1lem  9323  fisupcl  9360  ordtypelem3  9412  ordtypelem8  9417  oieu  9431  oismo  9432  wofib  9437  wemaplem2  9439  wemapso  9443  wemapso2lem  9444  unxpwdom2  9480  infdifsn  9553  oemapvali  9580  cantnflem1c  9583  cantnflem1  9585  cantnf  9589  cnfcom3  9600  r1ordg  9677  dif1card  9907  infxpenlem  9910  dfac8clem  9929  infxp  10111  infmap2  10114  cflim2  10160  coftr  10170  fin2i2  10215  enfin2i  10218  fin23lem26  10222  fin23lem27  10225  fin23lem40  10248  isf32lem2  10251  isf32lem3  10252  isf32lem4  10253  isf32lem7  10256  isf32lem9  10258  fin1a2lem13  10309  fin12  10310  alephexp1  10476  gchdomtri  10526  fpwwe2lem11  10538  fpwwe2lem12  10539  gchpwdom  10567  gchhar  10576  adderpqlem  10851  mulerpqlem  10852  addassnq  10855  mulassnq  10856  distrnq  10858  mulidnq  10860  recmulnq  10861  ltexnq  10872  distrlem1pr  10922  distrlem4pr  10923  prlem936  10944  reclem3pr  10946  mulcmpblnr  10968  mulgt0d  11274  mul4d  11331  add4d  11348  add42d  11349  subcan  11422  addsub4d  11525  subadd4d  11526  sub4d  11527  2addsubd  11528  addsubeq4d  11529  muladdd  11581  mulsubd  11582  addgegt0d  11696  addgtge0d  11697  addge0d  11699  mulge0d  11700  le2subd  11743  ltleaddd  11744  leltaddd  11745  lt2subd  11747  divdivdiv  11828  divcan5  11829  divne0d  11919  recdivd  11920  recdiv2d  11921  divcan6d  11922  ddcand  11923  rec11d  11924  divmuldivd  11944  divmul13d  11945  divmul24d  11946  divadddivd  11947  divsubdivd  11948  divmuleqd  11949  divdivdivd  11950  mulge0b  11998  recreclt  12027  divgt0d  12063  mulgt1d  12064  lemulge11d  12065  lemulge12d  12066  ltmul12ad  12069  lemul12ad  12070  lemul12bd  12071  supmul1  12097  nndivtr  12178  qreccl  12873  ledivdivd  12965  lediv12ad  12999  lt2mul2divd  13009  xlt2add  13165  supxrun  13221  supxrre  13232  infxrre  13242  elicore  13304  iccss2  13323  iccssico2  13326  icossico2d  13327  lincmb01cmp  13401  iccf1o  13402  fzrev2i  13495  2tnp1ge0ge0  13739  m1modnnsub1  13830  modaddmodup  13847  modaddmodlo  13848  modsubdir  13853  fzennn  13881  sermono  13947  mulexpz  14015  expaddz  14019  sqdiv  14034  expsubd  14070  ltexp2a  14079  expmordi  14080  leexp2a  14085  expmulnbnd  14148  digit1  14150  lt2sqd  14169  le2sqd  14170  sq11d  14171  bcm1k  14228  bcp1n  14229  bcp1nk  14230  hashf1lem1  14368  cshw1  14735  2swrd2eqwrdeq  14866  ofccat  14882  absrele  15221  sqreulem  15273  sqrtmuld  15338  sqrtsq2d  15339  sqrtled  15340  sqrtltd  15341  sqr11d  15342  abs3lemd  15377  rlimuni  15463  climuni  15465  lo1resb  15477  o1resb  15479  2clim  15485  addcn2  15507  mulcn2  15509  o1of2  15526  o1rlimmul  15532  lo1add  15540  lo1mul  15541  isercolllem1  15578  caucvgrlem  15586  iseraltlem2  15596  iseraltlem3  15597  mptfzshft  15691  fsumrev  15692  fsum0diag2  15696  binomlem  15742  climcndslem1  15762  climcndslem2  15763  harmonic  15772  mertenslem1  15797  fprodser  15862  fprodrev  15890  efcllem  15990  moddvds  16180  dvds1  16236  dvdsext  16238  evennn2n  16268  bitsinv1  16359  sadaddlem  16383  sadasslem  16387  sadeq  16389  mulgcd  16465  dvdssqlem  16483  lcmftp  16553  rpmulgcd2  16573  coprmproddvdslem  16579  isprm5  16624  isprm6  16631  crth  16695  eulerthlem2  16699  prmdiveq  16703  pythagtriplem11  16743  pythagtriplem13  16745  pcgcd1  16795  pcprmpw2  16800  pcaddlem  16806  fldivp1  16815  4sqlem12  16874  4sqlem14  16876  4sqlem15  16877  4sqlem16  16878  vdwapun  16892  mreexexlem4d  17559  acsfn1  17573  acsfn2  17575  sscpwex  17728  rescabs  17746  yonedainv  18193  chnub  18534  subm0  18729  pmtrfb  19383  psgnunilem1  19411  odmodnn0  19458  odeq  19468  dfod2  19482  sylow1lem1  19516  lsmsubg  19572  lsmmod  19593  lsmdisj2  19600  ghmplusg  19764  odadd  19768  gexexlem  19770  lt6abl  19813  cyggex2  19815  dprdfinv  19939  dmdprdsplitlem  19957  dpjidcl  19978  ablfacrp  19986  ablfacrp2  19987  ablfac1c  19991  ablfac1eu  19993  omndadd2d  20048  omndadd2rd  20049  omndmul2  20051  acsfn1p  20720  lcomfsupp  20841  lssvancl1  20884  lssvnegcl  20895  lspprvacl  20938  ellspsni  20940  lspsn  20941  lmhmplusg  20984  lmhmima  20987  lmhmpreima  20988  reslmhm  20992  lbsind2  21021  lsmcl  21023  lsmelval2  21025  lsppreli  21030  lspprabs  21035  pj1lmhm  21040  lssvs0or  21053  lspabs3  21064  lspfixed  21071  lspexch  21072  lsmcv  21084  lspsolv  21086  drngnidl  21186  rhmpreimaidl  21220  rngqiprngimfo  21244  rngqiprngfulem4  21257  gzrngunit  21376  zringlpirlem3  21407  prmirredlem  21415  znf1o  21494  znunithash  21507  freshmansdream  21517  ofldchr  21519  frlmsubgval  21708  frlmvplusgvalc  21710  frlmvscaval  21711  frlmphllem  21723  frlmphl  21724  frlmssuvc1  21737  frlmsslsp  21739  frlmup1  21741  frlmup2  21742  lindfind2  21761  lindfrn  21764  f1lindf  21765  islindf4  21781  mplbas2  21983  evlslem3  22021  evlslem1  22023  coe1addfv  22185  lply1binom  22231  evl1addd  22262  evl1subd  22263  evl1muld  22264  mamudi  22324  mamudir  22325  1marepvmarrepid  22496  mdetrlin  22523  smadiadetglem1  22592  smadiadetg  22594  cramerimplem1  22604  mat2pmatscmxcl  22661  m2pmfzgsumcl  22669  pmatcollpw  22702  pmatcollpwfi  22703  pmatcollpw3fi1lem1  22707  cpmidpmatlem2  22792  cpmadugsumlemF  22797  chcoeffeqlem  22806  ntrin  22982  topssnei  23045  restbas  23079  restntr  23103  cnntri  23192  fiuncmp  23325  nllyrest  23407  nllyidm  23410  hausllycmp  23415  cldllycmp  23416  hauspwdom  23422  txcld  23524  txcn  23547  txlly  23557  txnlly  23558  txhaus  23568  txlm  23569  txkgen  23573  xkococnlem  23580  cnmpt2res  23598  xkoinjcn  23608  basqtop  23632  qtopeu  23637  trfbas2  23764  neifil  23801  hausflim  23902  alexsubALTlem2  23969  cnextfval  23983  cnextfvval  23986  cnextf  23987  cnextfres  23990  clssubg  24030  utop2nei  24171  utop3cls  24172  utopreg  24173  psmetlecl  24236  xmetlecl  24267  prdsxmetlem  24289  bldisj  24319  imasf1obl  24409  prdsbl  24412  stdbdmet  24437  stdbdmopn  24439  met2ndci  24443  metcnp  24462  metustto  24474  metustexhalf  24477  cfilucfil  24480  metucn  24492  lssnlm  24622  nmotri  24660  nmoid  24663  tgioo  24717  blcvx  24719  xrsmopn  24734  reperflem  24740  reconnlem2  24749  opnreen  24753  metdsge  24771  metdsre  24775  metdscnlem  24777  metnrmlem1a  24780  metnrmlem1  24781  metnrmlem3  24783  cncfmet  24835  cnmpopc  24855  icopnfcnv  24873  icopnfhmeo  24874  cnllycmp  24888  evth  24891  lebnumii  24898  nmoleub2lem3  25048  iscfil2  25199  cfil3i  25202  iscfil3  25206  cfilfcls  25207  iscau3  25211  iscmet3lem2  25225  caubl  25241  lmcau  25246  cssbn  25308  rrxcph  25325  minveclem2  25359  pjthlem1  25370  pjthlem2  25371  ivthicc  25392  ovollecl  25417  ovolunlem1a  25430  ovolunnul  25434  ovoliunlem1  25436  ismbl2  25461  nulmbl2  25470  unmbl  25471  volun  25479  voliunlem2  25485  ioombl1lem2  25493  uniioombllem2a  25516  uniioombllem3  25519  uniioombllem4  25520  dyaddisjlem  25529  dyadmaxlem  25531  opnmbllem  25535  volsup2  25539  volcn  25540  ismbfd  25573  mbfi1fseqlem1  25649  mbfi1fseqlem5  25653  itg2lecl  25672  itg2monolem2  25685  itg2gt0  25694  itgspliticc  25771  ellimc3  25813  limcres  25820  dvfval  25831  dvres3  25847  dvres3a  25848  dvmptresicc  25850  dvnff  25858  dvnadd  25864  dvn2bss  25865  dvnres  25866  dvcmul  25880  dvcmulf  25881  dvmptres3  25893  dvmptres2  25899  dvmptntr  25908  dvexp3  25915  dvferm1lem  25921  dvlip  25931  dvlipcn  25932  dvlip2  25933  c1liplem1  25934  dvgt0lem1  25940  dvgt0lem2  25941  dvne0  25949  lhop1lem  25951  lhop2  25953  lhop  25954  dvcnvrelem1  25955  dvcnvrelem2  25956  dvcvx  25958  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumlem2  25966  dvfsumlem2OLD  25967  ftc1lem6  25981  ftc1  25982  ftc2ditglem  25985  itgsubstlem  25988  itgpowd  25990  tdeglem4  25998  mdegaddle  26012  mdegmullem  26016  ply1rem  26104  fta1glem2  26107  fta1blem  26109  ig1peu  26113  ig1pdvds  26118  dgrmulc  26210  dgrcolem1  26212  plydivlem4  26237  plydiveu  26239  fta1lem  26248  vieta1lem1  26251  vieta1lem2  26252  plyexmo  26254  taylfvallem1  26297  taylfval  26299  tayl0  26302  taylplem1  26303  taylply2  26308  taylply2OLD  26309  taylply  26310  dvtaylp  26311  dvntaylp  26312  dvntaylp0  26313  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulmcaulem  26336  ulmcau  26337  ulmcn  26341  ulmdvlem1  26342  radcnvlem1  26355  radcnvle  26362  psercn  26369  pserdvlem2  26371  pserdv  26372  abelth  26384  tanregt0  26481  dvlog2lem  26594  efopn  26600  logtayllem  26601  logccv  26605  cxplt3  26642  cxpmul2zd  26658  cxpltd  26661  cxpled  26662  cxplt3d  26677  cxple3d  26678  dvsqrt  26684  cxpcn3  26691  cxpaddle  26695  cxpeq  26700  angcan  26745  angvald  26747  ang180lem2  26753  ang180  26757  isosctrlem3  26763  dquartlem1  26794  atantayl2  26881  leibpi  26885  log2tlbnd  26888  birthdaylem3  26896  xrlimcnp  26911  efrlim  26912  efrlimOLD  26913  o1cxp  26918  jensenlem2  26931  jensen  26932  fsumharmonic  26955  lgamucov  26981  lgamcvg2  26998  wilthlem1  27011  basellem3  27026  basellem6  27029  basellem8  27031  ppisval  27047  chtwordi  27099  ppiwordi  27105  mumullem2  27123  mpodvdsmulf1o  27137  dvdsmulf1o  27139  fsumvma  27157  fsumvma2  27158  chpchtsum  27163  chpub  27164  logfacubnd  27165  dchrmulcl  27193  dchrinv  27205  dchrptlem1  27208  dchrptlem2  27209  sumdchr2  27214  dchr2sum  27217  bposlem7  27234  lgslem1  27241  lgslem3  27243  lgsdirprm  27275  lgsqrlem2  27291  lgseisenlem1  27319  lgseisenlem2  27320  lgseisenlem4  27322  lgseisen  27323  lgsquadlem1  27324  lgsquad2lem1  27328  lgsquad3  27331  m1lgs  27332  2sqlem7  27368  2sq2  27377  2sqmod  27380  chebbnd1lem2  27414  chebbnd1lem3  27415  rplogsumlem1  27428  rpvmasumlem  27431  dchrvmasumlem1  27439  dchrvmasum2lem  27440  dchrvmasumlema  27444  dchrisum0flblem2  27453  dchrisum0fno1  27455  dchrisum0re  27457  logdivsum  27477  pntrsumbnd2  27511  pntpbnd1a  27529  pntpbnd1  27530  pntibndlem2  27535  pntlemr  27546  pntlemj  27547  pntlemf  27549  pnt2  27557  padicabv  27574  ostth2lem2  27578  slerecd  27767  sltrecd  27769  madebday  27851  addsproplem6  27923  negsproplem6  27981  mulsproplem13  28073  mulsproplem14  28074  sltmuld  28082  mulsgt0d  28090  f1otrg  28855  brbtwn2  28890  colinearalglem2  28892  axcgrtr  28900  axcgrid  28901  axsegconlem7  28908  axsegcon  28912  ax5seglem3  28916  ax5seglem6  28919  ax5seg  28923  axpaschlem  28925  axlowdimlem17  28943  axcontlem2  28950  axcontlem4  28952  axcontlem7  28955  axcontlem8  28956  ecgrtg  28968  usgredg2v  29212  vtxdgoddnumeven  29539  2trlond  29924  eupthp1  30203  nmobndi  30762  ubthlem2  30858  ubthlem3  30859  minvecolem2  30862  shuni  31287  pjhthlem1  31378  chscllem2  31625  pjcompi  31659  mayete3i  31715  unoplin  31907  hmoplin  31929  nmophmi  32018  mdslmd4i  32320  isoun  32690  submuladdd  32730  receqid  32735  xrge0addcld  32752  xrofsup  32757  eliccelico  32767  elicoelioo  32768  difioo  32772  hashpss  32798  sgnmul  32825  rexdiv  32913  mgcmnt1d  32985  mgcmnt2d  32986  xrge0addgt0  33005  cycpmcl  33092  cycpm2tr  33095  cyc3evpm  33126  cycpmconjslem2  33131  fldgensdrg  33287  qusker  33321  eqgvscpbl  33322  ringlsmss1  33368  ringlsmss2  33369  lidlmcld  33391  intlidl  33392  lidlunitel  33395  elrspunidl  33400  idlinsubrg  33403  isprmidlc  33419  rhmpreimaprmidl  33423  qsidomlem1  33424  ssdifidllem  33428  mxidlmaxv  33440  mxidlprm  33442  ssmxidllem  33445  opprmxidlabs  33459  qsdrnglem2  33468  mplvrpmmhm  33583  mplvrpmrhm  33584  resssra  33606  ply1degltdimlem  33642  lindsunlem  33644  sdrgfldext  33670  fldsdrgfldext  33681  finexttrb  33685  fldgenfldext  33688  fldextrspunlem1  33695  algextdeglem4  33740  algextdeglem8  33744  constrextdg2lem  33768  mdetpmtr2  33844  mdetpmtr12  33845  madjusmdetlem1  33847  madjusmdetlem4  33850  rhmpreimacn  33905  unitdivcld  33921  xrge0mulc1cn  33961  qqhnm  34010  esumcst  34083  esumfsup  34090  esumpmono  34099  esumcvg  34106  difelsiga  34153  sigapisys  34175  sigapildsys  34182  ldgenpisyslem1  34183  1stmbfm  34280  2ndmbfm  34281  dya2icoseg  34297  sibfinima  34359  probmeasb  34450  orvcgteel  34488  orvclteel  34493  ballotlemsima  34536  ballotlemfrceq  34549  ccatmulgnn0dir  34562  fct2relem  34617  ftc2re  34618  chtvalz  34649  r1filimi  35121  subfacp1lem2a  35231  subfaclim  35239  erdsze2lem2  35255  cvmliftlem2  35337  cvmliftlem10  35345  cvmliftlem13  35347  cvmliftiota  35352  cvmlift2lem9  35362  cvmlift2lem11  35364  cvmlift2lem12  35365  cvmliftphtlem  35368  cvmlift3lem6  35375  cvmlift3lem7  35376  cvmlift3lem9  35378  snmlff  35380  mrsubfval  35559  wzel  35873  wsuclem  35874  brsegle  36159  opnregcld  36381  weiunfrlem  36515  fin2so  37653  poimirlem17  37683  poimirlem23  37689  opnmbllem0  37702  mblfinlem3  37705  mblfinlem4  37706  itg2addnclem  37717  itg2addnc  37720  itg2gt0cn  37721  ftc1cnnclem  37737  ftc1cnnc  37738  areacirclem5  37758  indexdom  37780  sstotbnd2  37820  isbnd3  37830  isbnd3b  37831  cntotbnd  37842  ismtyima  37849  heibor1lem  37855  heiborlem8  37864  rrncmslem  37878  reheibor  37885  lkrlsp  39207  lshpkrlem5  39219  ldualssvscl  39263  ldualssvsubcl  39264  llnmlplnN  39644  llncvrlpln  39663  pmapjat1  39958  pclfinN  40005  lautlt  40196  lauteq  40200  lautco  40202  ltrn11  40231  ltrnle  40234  ltrneq2  40253  cdlemednuN  40405  cdleme20k  40424  cdleme20l2  40426  cdleme20l  40427  cdleme20m  40428  cdleme21c  40432  cdleme22e  40449  cdleme22eALTN  40450  cdlemefrs32fva  40505  cdlemg4g  40721  cdlemg18b  40784  cdlemg18c  40785  cdlemj3  40928  dia2dimlem5  41173  dvhopN  41221  cdlemm10N  41223  dihjatcclem4  41526  dochexmidlem2  41566  lclkrlem2o  41626  lcfrlem5  41651  lcfrlem6  41652  lcdlssvscl  41711  mapdpglem6  41783  mapdpglem9  41785  mapdpglem12  41788  mapdpglem14  41790  mapdindp0  41824  hdmaprnlem7N  41960  hdmaprnlem8N  41961  hdmaprnlem3eN  41963  hgmapvvlem3  42030  dvun  42458  addinvcom  42531  evlsaddval  42667  evlsmulval  42668  evladdval  42674  evlmulval  42675  mzpsubst  42846  eldioph2lem1  42858  eldioph2lem2  42859  eldioph2b  42861  diophin  42870  irrapxlem2  42921  irrapxlem4  42923  irrapxlem5  42924  pellexlem1  42927  pellexlem2  42928  pellexlem6  42932  elpell1qr2  42970  pell1qrgaplem  42971  pell1qrgap  42972  pellqrex  42977  pellfundex  42984  pellfund14  42996  rmspecsqrtnq  43004  rmxyadd  43019  congsub  43068  mzpcong  43070  congrep  43071  acongtr  43076  acongrep  43078  jm2.19lem1  43087  jm2.22  43093  jm2.23  43094  jm2.26lem3  43099  jm2.26  43100  jm2.27a  43103  fnwe2lem2  43149  aomclem6  43157  hbtlem2  43222  hbtlem4  43224  hbtlem5  43226  dgraa0p  43247  rngunsnply  43267  proot1hash  43293  nnoeomeqom  43410  cantnf2  43423  omabs2  43430  naddcnff  43460  naddcnffo  43462  naddcnfcom  43464  naddcnfid1  43465  expgrowth  44433  fpmd  45365  abslt2sqd  45464  ioondisj2  45598  ioondisj1  45599  eliocre  45614  ioossioobi  45622  iooiinicc  45647  iooiinioc  45661  lptioo2  45736  limcresiooub  45745  limsupequzlem  45825  xlimmnfvlem2  45936  xlimpnfvlem2  45940  cncfuni  45989  cncfiooicclem1  45996  cxpcncf2  46002  dvcnre  46019  dvresntr  46021  dvresioo  46024  dvbdfbdioolem1  46031  dvnmptdivc  46041  dvnxpaek  46045  itgsinexplem1  46057  itgcoscmulx  46072  itgiccshift  46083  itgperiod  46084  ovolsplit  46091  stoweidlem11  46114  stoweidlem26  46129  stoweidlem34  46137  stoweidlem36  46139  stoweidlem38  46141  stirlinglem5  46181  dirkercncflem2  46207  dirkercncflem4  46209  fourierdlem20  46230  fourierdlem58  46267  fourierdlem72  46281  fourierdlem73  46282  fourierdlem74  46283  fourierdlem75  46284  fourierdlem76  46285  fourierdlem79  46288  fourierdlem80  46289  fourierdlem87  46296  fourierdlem94  46303  fourierdlem103  46312  fourierdlem104  46313  fourierdlem107  46316  fourierdlem113  46322  sqwvfoura  46331  sqwvfourb  46332  fourierswlem  46333  fouriersw  46334  etransclem46  46383  etransclem47  46384  rrndistlt  46393  rrnprjdstle  46404  ioorrnopnxrlem  46409  sge0ssre  46500  sge0seq  46549  hsphoidmvle2  46688  hsphoidmvle  46689  hoidmv1lelem1  46694  hoidmv1lelem2  46695  hoidmv1lelem3  46696  hoidmvlelem1  46698  hoidifhspdmvle  46723  hoiqssbllem2  46726  ovolval5lem2  46756  iinhoiicc  46777  iunhoiioo  46779  vonioolem2  46784  vonicclem2  46787  issmflem  46830  submodlt  47455  iccpartdisj  47542  m1expevenALTV  47752  fpprel2  47846  tgoldbach  47922  opstrgric  48031  gpg3kgrtriex  48194  nn0eo  48634  fdivpm  48649  refdivpm  48650  elbigolo1  48663  logbpw2m1  48673  fllog2  48674  dignn0flhalflem1  48721  dignn0flhalflem2  48722  itsclinecirc0in  48881  2itscplem2  48885  itscnhlinecirc02plem1  48888  iccdisj2  49002