Theorem syl22anc 849

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 519	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 847	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  preqsnd  4817  fr2nr  5624  soltmin  6123  f1oprg  6853  f1prex  7268  fveqf1o  7286  weniso  7338  fr3nr  7755  suppofssd  8183  smogt  8338  smocdmdom  8339  oacomf1o  8534  en2prd  9028  difsnen  9031  enfixsn  9058  domss2  9108  ssenen  9123  marypha1lem  9379  fisupcl  9416  ordtypelem3  9468  ordtypelem8  9473  oieu  9487  oismo  9488  wofib  9493  wemaplem2  9495  wemapso  9499  wemapso2lem  9500  unxpwdom2  9536  infdifsn  9612  oemapvali  9639  cantnflem1c  9642  cantnflem1  9644  cantnf  9648  cnfcom3  9659  r1ordg  9736  dif1card  9966  infxpenlem  9969  dfac8clem  9988  infxp  10170  infmap2  10173  cflim2  10220  coftr  10230  fin2i2  10275  enfin2i  10278  fin23lem26  10282  fin23lem27  10285  fin23lem40  10308  isf32lem2  10311  isf32lem3  10312  isf32lem4  10313  isf32lem7  10316  isf32lem9  10318  fin1a2lem13  10369  fin12  10370  alephexp1  10537  gchdomtri  10587  fpwwe2lem11  10599  fpwwe2lem12  10600  gchpwdom  10628  gchhar  10637  adderpqlem  10912  mulerpqlem  10913  addassnq  10916  mulassnq  10917  distrnq  10919  mulidnq  10921  recmulnq  10922  ltexnq  10933  distrlem1pr  10983  distrlem4pr  10984  prlem936  11005  reclem3pr  11007  mulcmpblnr  11029  mulgt0d  11338  mul4d  11395  add4d  11412  add42d  11413  subcan  11486  addsub4d  11589  subadd4d  11590  sub4d  11591  2addsubd  11592  addsubeq4d  11593  muladdd  11645  mulsubd  11646  addgegt0d  11760  addgtge0d  11761  addge0d  11763  mulge0d  11764  le2subd  11807  ltleaddd  11808  leltaddd  11809  lt2subd  11811  divdivdiv  11892  divcan5  11893  divne0d  11983  recdivd  11984  recdiv2d  11985  divcan6d  11986  ddcand  11987  rec11d  11988  divmuldivd  12008  divmul13d  12009  divmul24d  12010  divadddivd  12011  divsubdivd  12012  divmuleqd  12013  divdivdivd  12014  mulge0b  12062  recreclt  12091  divgt0d  12127  mulgt1d  12128  lemulge11d  12129  lemulge12d  12130  ltmul12ad  12133  lemul12ad  12134  lemul12bd  12135  supmul1  12161  nndivtr  12260  qreccl  12970  ledivdivd  13062  lediv12ad  13096  lt2mul2divd  13106  xlt2add  13263  supxrun  13319  supxrre  13330  infxrre  13340  elicore  13402  iccss2  13421  iccssico2  13424  icossico2d  13425  lincmb01cmp  13499  iccf1o  13500  nnge2recico01  13511  fzrev2i  13594  2tnp1ge0ge0  13839  m1modnnsub1  13930  modaddmodup  13947  modaddmodlo  13948  modsubdir  13953  fzennn  13981  sermono  14047  mulexpz  14115  expaddz  14119  sqdiv  14134  expsubd  14170  ltexp2a  14179  expmordi  14180  leexp2a  14185  expmulnbnd  14248  digit1  14250  lt2sqd  14269  le2sqd  14270  sq11d  14271  bcm1k  14328  bcp1n  14329  bcp1nk  14330  hashf1lem1  14468  cshw1  14835  2swrd2eqwrdeq  14966  ofccat  14982  sgnmul  15120  absrele  15335  sqreulem  15387  sqrtmuld  15452  sqrtsq2d  15453  sqrtled  15454  sqrtltd  15455  sqr11d  15456  abs3lemd  15491  rlimuni  15577  climuni  15579  lo1resb  15591  o1resb  15593  2clim  15599  addcn2  15621  mulcn2  15623  o1of2  15640  o1rlimmul  15646  lo1add  15654  lo1mul  15655  isercolllem1  15692  caucvgrlem  15700  iseraltlem2  15710  iseraltlem3  15711  mptfzshft  15805  fsumrev  15806  fsum0diag2  15810  binomlem  15859  climcndslem1  15879  climcndslem2  15880  harmonic  15889  mertenslem1  15914  fprodser  15979  fprodrev  16007  efcllem  16107  moddvds  16297  dvds1  16353  dvdsext  16355  evennn2n  16385  bitsinv1  16476  sadaddlem  16500  sadasslem  16504  sadeq  16506  mulgcd  16582  dvdssqlem  16600  lcmftp  16670  rpmulgcd2  16690  coprmproddvdslem  16696  isprm5  16742  isprm6  16749  crth  16813  eulerthlem2  16817  prmdiveq  16821  pythagtriplem11  16861  pythagtriplem13  16863  pcgcd1  16913  pcprmpw2  16918  pcaddlem  16924  fldivp1  16933  4sqlem12  16992  4sqlem14  16994  4sqlem15  16995  4sqlem16  16996  vdwapun  17010  mreexexlem4d  17679  acsfn1  17693  acsfn2  17695  sscpwex  17848  rescabs  17866  yonedainv  18313  chnub  18654  subm0  18849  pmtrfb  19505  psgnunilem1  19533  odmodnn0  19580  odeq  19590  dfod2  19604  sylow1lem1  19638  lsmsubg  19694  lsmmod  19715  lsmdisj2  19722  ghmplusg  19886  odadd  19890  gexexlem  19892  lt6abl  19935  cyggex2  19937  dprdfinv  20061  dmdprdsplitlem  20079  dpjidcl  20100  ablfacrp  20108  ablfacrp2  20109  ablfac1c  20113  ablfac1eu  20115  omndadd2d  20170  omndadd2rd  20171  omndmul2  20173  acsfn1p  20845  lcomfsupp  20966  lssvancl1  21009  lssvnegcl  21020  lspprvacl  21063  ellspsni  21065  lspsn  21066  lmhmplusg  21108  lmhmima  21111  lmhmpreima  21112  reslmhm  21116  lbsind2  21145  lsmcl  21147  lsmelval2  21149  lsppreli  21154  lspprabs  21159  pj1lmhm  21164  lssvs0or  21177  lspabs3  21188  lspfixed  21195  lspexch  21196  lsmcv  21208  lspsolv  21210  drngnidl  21310  rhmpreimaidl  21344  rngqiprngimfo  21368  rngqiprngfulem4  21381  gzrngunit  21482  zringlpirlem3  21513  prmirredlem  21521  znf1o  21600  znunithash  21613  freshmansdream  21623  ofldchr  21625  frlmsubgval  21814  frlmvplusgvalc  21816  frlmvscaval  21817  frlmphllem  21829  frlmphl  21830  frlmssuvc1  21843  frlmsslsp  21845  frlmup1  21847  frlmup2  21848  lindfind2  21867  lindfrn  21870  f1lindf  21871  islindf4  21887  mplbas2  22092  evlslem3  22130  evlslem1  22132  evladdval  22153  evlmulval  22154  evlsaddval  22179  evlsmulval  22180  coe1addfv  22325  lply1binom  22370  evl1addd  22401  evl1subd  22402  evl1muld  22403  mamudi  22460  mamudir  22461  1marepvmarrepid  22632  mdetrlin  22659  smadiadetglem1  22728  smadiadetg  22730  cramerimplem1  22740  mat2pmatscmxcl  22797  m2pmfzgsumcl  22805  pmatcollpw  22838  pmatcollpwfi  22839  pmatcollpw3fi1lem1  22843  cpmidpmatlem2  22928  cpmadugsumlemF  22933  chcoeffeqlem  22942  ntrin  23118  topssnei  23181  restbas  23215  restntr  23239  cnntri  23328  fiuncmp  23461  nllyrest  23543  nllyidm  23546  hausllycmp  23551  cldllycmp  23552  hauspwdom  23558  txcld  23660  txcn  23683  txlly  23693  txnlly  23694  txhaus  23704  txlm  23705  txkgen  23709  xkococnlem  23716  cnmpt2res  23734  xkoinjcn  23744  basqtop  23768  qtopeu  23773  trfbas2  23900  neifil  23937  hausflim  24038  alexsubALTlem2  24105  cnextfval  24119  cnextfvval  24122  cnextf  24123  cnextfres  24126  clssubg  24166  utop2nei  24307  utop3cls  24308  utopreg  24309  psmetlecl  24372  xmetlecl  24403  prdsxmetlem  24425  bldisj  24455  imasf1obl  24545  prdsbl  24548  stdbdmet  24573  stdbdmopn  24575  met2ndci  24579  metcnp  24598  metustto  24610  metustexhalf  24613  cfilucfil  24616  metucn  24628  lssnlm  24758  nmotri  24796  nmoid  24799  tgioo  24853  blcvx  24855  xrsmopn  24870  reperflem  24876  reconnlem2  24885  opnreen  24889  metdsge  24907  metdsre  24911  metdscnlem  24913  metnrmlem1a  24916  metnrmlem1  24917  metnrmlem3  24919  cncfmet  24968  cnmpopc  24987  icopnfcnv  25001  icopnfhmeo  25002  cnllycmp  25015  evth  25018  lebnumii  25025  nmoleub2lem3  25174  iscfil2  25325  cfil3i  25328  iscfil3  25332  cfilfcls  25333  iscau3  25337  iscmet3lem2  25351  caubl  25367  lmcau  25372  cssbn  25434  rrxcph  25451  minveclem2  25485  pjthlem1  25496  pjthlem2  25497  ivthicc  25517  ovollecl  25542  ovolunlem1a  25555  ovolunnul  25559  ovoliunlem1  25561  ismbl2  25586  nulmbl2  25595  unmbl  25596  volun  25604  voliunlem2  25610  ioombl1lem2  25618  uniioombllem2a  25641  uniioombllem3  25644  uniioombllem4  25645  dyaddisjlem  25654  dyadmaxlem  25656  opnmbllem  25660  volsup2  25664  volcn  25665  ismbfd  25698  mbfi1fseqlem1  25774  mbfi1fseqlem5  25778  itg2lecl  25797  itg2monolem2  25810  itg2gt0  25819  itgspliticc  25896  ellimc3  25938  limcres  25945  dvfval  25956  dvres3  25972  dvres3a  25973  dvmptresicc  25975  dvnff  25982  dvnadd  25988  dvn2bss  25989  dvnres  25990  dvcmul  26003  dvcmulf  26004  dvmptres3  26015  dvmptres2  26021  dvmptntr  26030  dvexp3  26037  dvferm1lem  26043  dvlip  26052  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  dvgt0lem1  26061  dvgt0lem2  26062  dvne0  26070  lhop1lem  26072  lhop2  26074  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcvx  26079  dvfsumle  26080  dvfsumabs  26082  dvfsumlem2  26086  ftc1lem6  26100  ftc1  26101  ftc2ditglem  26104  itgsubstlem  26107  itgpowd  26109  tdeglem4  26117  mdegaddle  26131  mdegmullem  26135  ply1rem  26223  fta1glem2  26226  fta1blem  26228  ig1peu  26232  ig1pdvds  26237  dgrmulc  26328  dgrcolem1  26330  plydivlem4  26357  plydiveu  26359  fta1lem  26368  vieta1lem1  26371  vieta1lem2  26372  plyexmo  26374  taylfvallem1  26417  taylfval  26419  tayl0  26422  taylplem1  26423  taylply2  26428  taylply  26429  dvtaylp  26430  dvntaylp  26431  dvntaylp0  26432  taylthlem1  26433  taylthlem2  26434  ulmcaulem  26454  ulmcau  26455  ulmcn  26459  ulmdvlem1  26460  radcnvlem1  26473  radcnvle  26480  psercn  26486  pserdvlem2  26488  pserdv  26489  abelth  26501  tanregt0  26601  dvlog2lem  26714  efopn  26720  logtayllem  26721  logccv  26725  cxplt3  26762  cxpmul2zd  26778  cxpltd  26781  cxpled  26782  cxplt3d  26797  cxple3d  26798  dvsqrt  26804  cxpcn3  26810  cxpaddle  26814  cxpeq  26819  angcan  26864  angvald  26866  ang180lem2  26872  ang180  26876  isosctrlem3  26882  dquartlem1  26913  atantayl2  27000  leibpi  27004  log2tlbnd  27007  birthdaylem3  27015  xrlimcnp  27030  efrlim  27031  o1cxp  27036  jensenlem2  27049  jensen  27050  fsumharmonic  27073  lgamucov  27099  lgamcvg2  27116  wilthlem1  27129  basellem3  27144  basellem6  27147  basellem8  27149  ppisval  27165  chtwordi  27217  ppiwordi  27223  mumullem2  27241  mpodvdsmulf1o  27255  dvdsmulf1o  27257  fsumvma  27274  fsumvma2  27275  chpchtsum  27280  chpub  27281  logfacubnd  27282  dchrmulcl  27310  dchrinv  27322  dchrptlem1  27325  dchrptlem2  27326  sumdchr2  27331  dchr2sum  27334  bposlem7  27351  lgslem1  27358  lgslem3  27360  lgsdirprm  27392  lgsqrlem2  27408  lgseisenlem1  27436  lgseisenlem2  27437  lgseisenlem4  27439  lgseisen  27440  lgsquadlem1  27441  lgsquad2lem1  27445  lgsquad3  27448  m1lgs  27449  2sqlem7  27485  2sq2  27494  2sqmod  27497  chebbnd1lem2  27531  chebbnd1lem3  27532  rplogsumlem1  27545  rpvmasumlem  27548  dchrvmasumlem1  27556  dchrvmasum2lem  27557  dchrvmasumlema  27561  dchrisum0flblem2  27570  dchrisum0fno1  27572  dchrisum0re  27574  logdivsum  27594  pntrsumbnd2  27628  pntpbnd1a  27646  pntpbnd1  27647  pntibndlem2  27652  pntlemr  27663  pntlemj  27664  pntlemf  27666  pnt2  27674  padicabv  27691  ostth2lem2  27695  lesrecd  27890  ltsrecd  27892  madebday  27990  addsproplem6  28064  negsproplem6  28123  mulsproplem13  28218  mulsproplem14  28219  ltmulsd  28227  mulsgt0d  28235  f1otrg  29068  brbtwn2  29103  colinearalglem2  29105  axcgrtr  29113  axcgrid  29114  axsegconlem7  29121  axsegcon  29125  ax5seglem3  29129  ax5seglem6  29132  ax5seg  29136  axpaschlem  29138  axlowdimlem17  29156  axcontlem2  29163  axcontlem4  29165  axcontlem7  29168  axcontlem8  29169  ecgrtg  29181  usgredg2v  29425  vtxdgoddnumeven  29751  2trlond  30136  eupthp1  30415  nmobndi  30975  ubthlem2  31071  ubthlem3  31072  minvecolem2  31075  shuni  31500  pjhthlem1  31591  chscllem2  31838  pjcompi  31872  mayete3i  31928  unoplin  32120  hmoplin  32142  nmophmi  32231  mdslmd4i  32533  isoun  32901  submuladdd  32939  receqid  32943  xrge0addcld  32961  xrofsup  32966  eliccelico  32976  elicoelioo  32977  difioo  32981  hashpss  33008  rexdiv  33100  mgcmnt1d  33172  mgcmnt2d  33173  xrge0addgt0  33192  cycpmcl  33293  cycpm2tr  33296  cyc3evpm  33327  cycpmconjslem2  33332  fldgensdrg  33498  qusker  33532  eqgvscpbl  33533  ringlsmss1  33579  ringlsmss2  33580  lidlmcld  33602  intlidl  33603  lidlunitel  33606  elrspunidl  33611  idlinsubrg  33614  isprmidlc  33630  rhmpreimaprmidl  33635  qsidomlem1  33636  ssdifidllem  33640  mxidlmaxv  33653  mxidlprm  33655  ssmxidllem  33658  opprmxidlabs  33672  qsdrnglem2  33681  dflring3  33690  dflring4  33691  selvply1rhmlem4  33817  mplvrpmmhm  33840  mplvrpmrhm  33841  esplyind  33869  resssra  33881  ply1degltdimlem  33916  lindsunlem  33918  sdrgfldext  33944  fldsdrgfldext  33955  finexttrb  33959  fldgenfldext  33962  fldextrspunlem1  33969  algextdeglem4  34014  algextdeglem8  34018  constrextdg2lem  34042  mdetpmtr2  34118  mdetpmtr12  34119  madjusmdetlem1  34121  madjusmdetlem4  34124  rhmpreimacn  34179  unitdivcld  34195  xrge0mulc1cn  34235  qqhnm  34284  esumcst  34357  esumfsup  34364  esumpmono  34373  esumcvg  34380  difelsiga  34427  sigapisys  34449  sigapildsys  34456  ldgenpisyslem1  34457  1stmbfm  34554  2ndmbfm  34555  dya2icoseg  34571  sibfinima  34633  probmeasb  34724  orvcgteel  34762  orvclteel  34767  ballotlemsima  34810  ballotlemfrceq  34823  ccatmulgnn0dir  34836  fct2relem  34888  ftc2re  34889  chtvalz  34920  r1filimi  35396  subfacp1lem2a  35527  subfaclim  35535  erdsze2lem2  35551  cvmliftlem2  35633  cvmliftlem10  35641  cvmliftlem13  35643  cvmliftiota  35648  cvmlift2lem9  35658  cvmlift2lem11  35660  cvmlift2lem12  35661  cvmliftphtlem  35664  cvmlift3lem6  35671  cvmlift3lem7  35672  cvmlift3lem9  35674  snmlff  35676  mrsubfval  35855  wzel  36169  wsuclem  36170  brsegle  36455  opnregcld  36687  weiunfrlem  36821  fin2so  38103  poimirlem17  38133  poimirlem23  38139  opnmbllem0  38152  mblfinlem3  38155  mblfinlem4  38156  itg2addnclem  38167  itg2addnc  38170  itg2gt0cn  38171  ftc1cnnclem  38187  ftc1cnnc  38188  areacirclem5  38208  indexdom  38230  sstotbnd2  38270  isbnd3  38280  isbnd3b  38281  cntotbnd  38292  ismtyima  38299  heibor1lem  38305  heiborlem8  38314  rrncmslem  38328  reheibor  38335  lkrlsp  39723  lshpkrlem5  39735  ldualssvscl  39779  ldualssvsubcl  39780  llnmlplnN  40160  llncvrlpln  40179  pmapjat1  40474  pclfinN  40521  lautlt  40712  lauteq  40716  lautco  40718  ltrn11  40747  ltrnle  40750  ltrneq2  40769  cdlemednuN  40921  cdleme20k  40940  cdleme20l2  40942  cdleme20l  40943  cdleme20m  40944  cdleme21c  40948  cdleme22e  40965  cdleme22eALTN  40966  cdlemefrs32fva  41021  cdlemg4g  41237  cdlemg18b  41300  cdlemg18c  41301  cdlemj3  41444  dia2dimlem5  41689  dvhopN  41737  cdlemm10N  41739  dihjatcclem4  42042  dochexmidlem2  42082  lclkrlem2o  42142  lcfrlem5  42167  lcfrlem6  42168  lcdlssvscl  42227  mapdpglem6  42299  mapdpglem9  42301  mapdpglem12  42304  mapdpglem14  42306  mapdindp0  42340  hdmaprnlem7N  42476  hdmaprnlem8N  42477  hdmaprnlem3eN  42479  hgmapvvlem3  42546  dvun  42965  addinvcom  43038  mzpsubst  43326  eldioph2lem1  43338  eldioph2lem2  43339  eldioph2b  43341  diophin  43350  irrapxlem2  43397  irrapxlem4  43399  irrapxlem5  43400  pellexlem1  43403  pellexlem2  43404  pellexlem6  43408  elpell1qr2  43446  pell1qrgaplem  43447  pell1qrgap  43448  pellqrex  43453  pellfundex  43460  pellfund14  43472  rmspecsqrtnq  43480  rmxyadd  43495  congsub  43544  mzpcong  43546  congrep  43547  acongtr  43552  acongrep  43554  jm2.19lem1  43563  jm2.22  43569  jm2.23  43570  jm2.26lem3  43575  jm2.26  43576  jm2.27a  43579  fnwe2lem2  43625  aomclem6  43633  hbtlem2  43698  hbtlem4  43700  hbtlem5  43702  dgraa0p  43723  rngunsnply  43743  proot1hash  43769  nnoeomeqom  43886  cantnf2  43899  omabs2  43906  naddcnff  43936  naddcnffo  43938  naddcnfcom  43940  naddcnfid1  43941  expgrowth  44908  fpmd  45835  abslt2sqd  45933  ioondisj2  46066  ioondisj1  46067  eliocre  46082  ioossioobi  46090  iooiinicc  46115  iooiinioc  46129  lptioo2  46204  limcresiooub  46213  limsupequzlem  46293  xlimmnfvlem2  46404  xlimpnfvlem2  46408  cncfuni  46457  cncfiooicclem1  46464  cxpcncf2  46470  dvcnre  46487  dvresntr  46489  dvresioo  46492  dvbdfbdioolem1  46499  dvnmptdivc  46509  dvnxpaek  46513  itgsinexplem1  46525  itgcoscmulx  46540  itgiccshift  46551  itgperiod  46552  ovolsplit  46559  stoweidlem11  46582  stoweidlem26  46597  stoweidlem34  46605  stoweidlem36  46607  stoweidlem38  46609  stirlinglem5  46649  dirkercncflem2  46675  dirkercncflem4  46677  fourierdlem20  46698  fourierdlem58  46735  fourierdlem72  46749  fourierdlem73  46750  fourierdlem74  46751  fourierdlem75  46752  fourierdlem76  46753  fourierdlem79  46756  fourierdlem80  46757  fourierdlem87  46764  fourierdlem94  46771  fourierdlem103  46780  fourierdlem104  46781  fourierdlem107  46784  fourierdlem113  46790  sqwvfoura  46799  sqwvfourb  46800  fourierswlem  46801  fouriersw  46802  etransclem46  46851  etransclem47  46852  rrndistlt  46861  rrnprjdstle  46872  ioorrnopnxrlem  46877  sge0ssre  46968  sge0seq  47017  hsphoidmvle2  47156  hsphoidmvle  47157  hoidmv1lelem1  47162  hoidmv1lelem2  47163  hoidmv1lelem3  47164  hoidmvlelem1  47166  hoidifhspdmvle  47191  hoiqssbllem2  47194  ovolval5lem2  47224  iinhoiicc  47245  iunhoiioo  47247  vonioolem2  47252  vonicclem2  47255  issmflem  47298  submodlt  47947  iccpartdisj  48040  m1expevenALTV  48266  fpprel2  48360  tgoldbach  48436  opstrgric  48545  gpg3kgrtriex  48708  nn0eo  49147  fdivpm  49162  refdivpm  49163  elbigolo1  49176  logbpw2m1  49186  fllog2  49187  dignn0flhalflem1  49234  dignn0flhalflem2  49235  itsclinecirc0in  49394  2itscplem2  49398  itscnhlinecirc02plem1  49401  iccdisj2  49515