Theorem syl22anc 851

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  preqsnd  4828  fr2nr  5641  soltmin  6139  f1oprg  6870  f1prex  7285  fveqf1o  7303  weniso  7355  fr3nr  7773  suppofssd  8201  smogt  8356  smocdmdom  8357  oacomf1o  8552  en2prd  9046  difsnen  9049  enfixsn  9076  domss2  9126  ssenen  9141  marypha1lem  9395  fisupcl  9432  ordtypelem3  9484  ordtypelem8  9489  oieu  9503  oismo  9504  wofib  9509  wemaplem2  9511  wemapso  9515  wemapso2lem  9516  unxpwdom2  9552  infdifsn  9628  oemapvali  9655  cantnflem1c  9658  cantnflem1  9660  cantnf  9664  cnfcom3  9675  r1ordg  9752  dif1card  9996  infxpenlem  9999  dfac8clem  10018  infxp  10199  infmap2  10202  cflim2  10249  coftr  10259  fin2i2  10304  enfin2i  10307  fin23lem26  10311  fin23lem27  10314  fin23lem40  10337  isf32lem2  10340  isf32lem3  10341  isf32lem4  10342  isf32lem7  10345  isf32lem9  10347  fin1a2lem13  10398  fin12  10399  alephexp1  10566  gchdomtri  10616  fpwwe2lem11  10628  fpwwe2lem12  10629  gchpwdom  10657  gchhar  10666  adderpqlem  10941  mulerpqlem  10942  addassnq  10945  mulassnq  10946  distrnq  10948  mulidnq  10950  recmulnq  10951  ltexnq  10962  distrlem1pr  11012  distrlem4pr  11013  prlem936  11034  reclem3pr  11036  mulcmpblnr  11058  mulgt0d  11367  mul4d  11424  add4d  11441  add42d  11442  subcan  11515  addsub4d  11618  subadd4d  11619  sub4d  11620  2addsubd  11621  addsubeq4d  11622  muladdd  11674  mulsubd  11675  addgegt0d  11789  addgtge0d  11790  addge0d  11792  mulge0d  11793  le2subd  11836  ltleaddd  11837  leltaddd  11838  lt2subd  11840  divdivdiv  11918  divcan5  11919  divne0d  12009  recdivd  12010  recdiv2d  12011  divcan6d  12012  ddcand  12013  rec11d  12014  divmuldivd  12034  divmul13d  12035  divmul24d  12036  divadddivd  12037  divsubdivd  12038  divmuleqd  12039  divdivdivd  12040  mulge0b  12087  recreclt  12116  divgt0d  12152  mulgt1d  12153  lemulge11d  12154  lemulge12d  12155  ltmul12ad  12158  lemul12ad  12159  lemul12bd  12160  supmul1  12186  nndivtr  12285  qreccl  12995  ledivdivd  13087  lediv12ad  13121  lt2mul2divd  13131  xlt2add  13288  supxrun  13344  supxrre  13355  infxrre  13365  elicore  13427  iccss2  13446  iccssico2  13449  icossico2d  13450  lincmb01cmp  13524  iccf1o  13525  nnge2recico01  13536  fzrev2i  13619  2tnp1ge0ge0  13864  m1modnnsub1  13955  modaddmodup  13972  modaddmodlo  13973  modsubdir  13978  fzennn  14006  sermono  14072  mulexpz  14140  expaddz  14144  sqdiv  14159  expsubd  14195  ltexp2a  14204  expmordi  14205  leexp2a  14210  expmulnbnd  14273  digit1  14275  lt2sqd  14294  le2sqd  14295  sq11d  14296  bcm1k  14353  bcp1n  14354  bcp1nk  14355  hashpss  14448  hashf1lem1  14494  cshw1  14861  2swrd2eqwrdeq  14992  ofccat  15008  sgnmul  15146  absrele  15361  sqreulem  15413  sqrtmuld  15478  sqrtsq2d  15479  sqrtled  15480  sqrtltd  15481  sqr11d  15482  abs3lemd  15517  rlimuni  15603  climuni  15605  lo1resb  15617  o1resb  15619  2clim  15625  addcn2  15647  mulcn2  15649  o1of2  15666  o1rlimmul  15672  lo1add  15680  lo1mul  15681  isercolllem1  15718  caucvgrlem  15726  iseraltlem2  15736  iseraltlem3  15737  mptfzshft  15831  fsumrev  15832  fsum0diag2  15836  binomlem  15885  climcndslem1  15905  climcndslem2  15906  harmonic  15915  mertenslem1  15940  fprodser  16005  fprodrev  16033  efcllem  16133  moddvds  16323  dvds1  16379  dvdsext  16381  evennn2n  16411  bitsinv1  16502  sadaddlem  16526  sadasslem  16530  sadeq  16532  mulgcd  16608  dvdssqlem  16626  lcmftp  16696  rpmulgcd2  16716  coprmproddvdslem  16722  isprm5  16768  isprm6  16775  crth  16839  eulerthlem2  16843  prmdiveq  16847  pythagtriplem11  16887  pythagtriplem13  16889  pcgcd1  16939  pcprmpw2  16944  pcaddlem  16950  fldivp1  16959  4sqlem12  17018  4sqlem14  17020  4sqlem15  17021  4sqlem16  17022  vdwapun  17036  mreexexlem4d  17705  acsfn1  17719  acsfn2  17721  sscpwex  17874  rescabs  17892  yonedainv  18339  chnub  18680  subm0  18876  pmtrfb  19537  psgnunilem1  19565  odmodnn0  19612  odeq  19622  dfod2  19636  sylow1lem1  19670  lsmsubg  19726  lsmmod  19747  lsmdisj2  19754  ghmplusg  19918  odadd  19922  gexexlem  19924  lt6abl  19967  cyggex2  19969  dprdfinv  20093  dmdprdsplitlem  20111  dpjidcl  20132  ablfacrp  20140  ablfacrp2  20141  ablfac1c  20145  ablfac1eu  20147  omndadd2d  20202  omndadd2rd  20203  omndmul2  20205  acsfn1p  20882  lcomfsupp  21003  lssvancl1  21046  lssvnegcl  21057  lspprvacl  21100  ellspsni  21102  lspsn  21103  lmhmplusg  21145  lmhmima  21148  lmhmpreima  21149  reslmhm  21153  lbsind2  21182  lsmcl  21184  lsmelval2  21186  lsppreli  21191  lspprabs  21196  pj1lmhm  21201  lssvs0or  21214  lspabs3  21225  lspfixed  21232  lspexch  21233  lsmcv  21245  lspsolv  21247  lidlmcld  21332  drngnidl  21353  rhmpreimaidl  21389  rngqiprngimfo  21414  rngqiprngfulem4  21427  isprmidlc  21445  rhmpreimaprmidl  21450  qsidomlem1  21451  ssdifidllem  21455  gzrngunit  21554  zringlpirlem3  21585  prmirredlem  21593  znf1o  21672  znunithash  21685  freshmansdream  21695  ofldchr  21697  frlmsubgval  21886  frlmvplusgvalc  21888  frlmvscaval  21889  frlmphllem  21901  frlmphl  21902  frlmssuvc1  21915  frlmsslsp  21917  frlmup1  21919  frlmup2  21920  lindfind2  21939  lindfrn  21942  f1lindf  21943  islindf4  21959  mplbas2  22164  evlslem3  22202  evlslem1  22204  evladdval  22225  evlmulval  22226  evlsaddval  22251  evlsmulval  22252  coe1addfv  22397  lply1binom  22441  evl1addd  22472  evl1subd  22473  evl1muld  22474  mamudi  22531  mamudir  22532  1marepvmarrepid  22703  mdetrlin  22730  smadiadetglem1  22799  smadiadetg  22801  cramerimplem1  22811  mat2pmatscmxcl  22868  m2pmfzgsumcl  22876  pmatcollpw  22909  pmatcollpwfi  22910  pmatcollpw3fi1lem1  22914  cpmidpmatlem2  22999  cpmadugsumlemF  23004  chcoeffeqlem  23013  ntrin  23189  topssnei  23252  restbas  23286  restntr  23310  cnntri  23399  fiuncmp  23532  nllyrest  23614  nllyidm  23617  hausllycmp  23622  cldllycmp  23623  hauspwdom  23629  txcld  23731  txcn  23754  txlly  23764  txnlly  23765  txhaus  23775  txlm  23776  txkgen  23780  xkococnlem  23787  cnmpt2res  23805  xkoinjcn  23815  basqtop  23839  qtopeu  23844  trfbas2  23971  neifil  24008  hausflim  24109  alexsubALTlem2  24176  cnextfval  24190  cnextfvval  24193  cnextf  24194  cnextfres  24197  clssubg  24237  utop2nei  24378  utop3cls  24379  utopreg  24380  psmetlecl  24443  xmetlecl  24474  prdsxmetlem  24496  bldisj  24526  imasf1obl  24616  prdsbl  24619  stdbdmet  24644  stdbdmopn  24646  met2ndci  24650  metcnp  24669  metustto  24681  metustexhalf  24684  cfilucfil  24687  metucn  24699  lssnlm  24829  nmotri  24867  nmoid  24870  tgioo  24924  blcvx  24926  xrsmopn  24941  reperflem  24947  reconnlem2  24956  opnreen  24960  metdsge  24978  metdsre  24982  metdscnlem  24984  metnrmlem1a  24987  metnrmlem1  24988  metnrmlem3  24990  cncfmet  25039  cnmpopc  25058  icopnfcnv  25072  icopnfhmeo  25073  cnllycmp  25086  evth  25089  lebnumii  25096  nmoleub2lem3  25245  iscfil2  25396  cfil3i  25399  iscfil3  25403  cfilfcls  25404  iscau3  25408  iscmet3lem2  25422  caubl  25438  lmcau  25443  cssbn  25505  rrxcph  25522  minveclem2  25556  pjthlem1  25567  pjthlem2  25568  ivthicc  25588  ovollecl  25613  ovolunlem1a  25626  ovolunnul  25630  ovoliunlem1  25632  ismbl2  25657  nulmbl2  25666  unmbl  25667  volun  25675  voliunlem2  25681  ioombl1lem2  25689  uniioombllem2a  25712  uniioombllem3  25715  uniioombllem4  25716  dyaddisjlem  25725  dyadmaxlem  25727  opnmbllem  25731  volsup2  25735  volcn  25736  ismbfd  25769  mbfi1fseqlem1  25845  mbfi1fseqlem5  25849  itg2lecl  25868  itg2monolem2  25881  itg2gt0  25890  itgspliticc  25967  ellimc3  26009  limcres  26016  dvfval  26027  dvres3  26043  dvres3a  26044  dvmptresicc  26046  dvnff  26053  dvnadd  26059  dvn2bss  26060  dvnres  26061  dvcmul  26074  dvcmulf  26075  dvmptres3  26086  dvmptres2  26092  dvmptntr  26101  dvexp3  26108  dvferm1lem  26114  dvlip  26123  dvlipcn  26124  dvlip2  26125  c1liplem1  26126  dvgt0lem1  26132  dvgt0lem2  26133  dvne0  26141  lhop1lem  26143  lhop2  26145  lhop  26146  dvcnvrelem1  26147  dvcnvrelem2  26148  dvcvx  26150  dvfsumle  26151  dvfsumabs  26153  dvfsumlem2  26157  ftc1lem6  26171  ftc1  26172  ftc2ditglem  26175  itgsubstlem  26178  itgpowd  26180  tdeglem4  26188  mdegaddle  26202  mdegmullem  26206  ply1rem  26294  fta1glem2  26297  fta1blem  26299  ig1peu  26303  ig1pdvds  26308  dgrmulc  26399  dgrcolem1  26401  plydivlem4  26428  plydiveu  26430  fta1lem  26439  vieta1lem1  26442  vieta1lem2  26443  plyexmo  26445  taylfvallem1  26488  taylfval  26490  tayl0  26493  taylplem1  26494  taylply2  26499  taylply  26500  dvtaylp  26501  dvntaylp  26502  dvntaylp0  26503  taylthlem1  26504  taylthlem2  26505  ulmcaulem  26525  ulmcau  26526  ulmcn  26530  ulmdvlem1  26531  radcnvlem1  26544  radcnvle  26551  psercn  26557  pserdvlem2  26559  pserdv  26560  abelth  26572  tanregt0  26672  dvlog2lem  26785  efopn  26791  logtayllem  26792  logccv  26796  cxplt3  26833  cxpmul2zd  26849  cxpltd  26852  cxpled  26853  cxplt3d  26868  cxple3d  26869  dvsqrt  26875  cxpcn3  26881  cxpaddle  26885  cxpeq  26890  angcan  26935  angvald  26937  ang180lem2  26943  ang180  26947  isosctrlem3  26953  dquartlem1  26984  atantayl2  27071  leibpi  27075  log2tlbnd  27078  birthdaylem3  27086  xrlimcnp  27101  efrlim  27102  o1cxp  27107  jensenlem2  27120  jensen  27121  fsumharmonic  27144  lgamucov  27170  lgamcvg2  27187  wilthlem1  27200  basellem3  27215  basellem6  27218  basellem8  27220  ppisval  27236  chtwordi  27288  ppiwordi  27294  mumullem2  27312  mpodvdsmulf1o  27326  dvdsmulf1o  27328  fsumvma  27345  fsumvma2  27346  chpchtsum  27351  chpub  27352  logfacubnd  27353  dchrmulcl  27381  dchrinv  27393  dchrptlem1  27396  dchrptlem2  27397  sumdchr2  27402  dchr2sum  27405  bposlem7  27422  lgslem1  27429  lgslem3  27431  lgsdirprm  27463  lgsqrlem2  27479  lgseisenlem1  27507  lgseisenlem2  27508  lgseisenlem4  27510  lgseisen  27511  lgsquadlem1  27512  lgsquad2lem1  27516  lgsquad3  27519  m1lgs  27520  2sqlem7  27556  2sq2  27565  2sqmod  27568  chebbnd1lem2  27602  chebbnd1lem3  27603  rplogsumlem1  27616  rpvmasumlem  27619  dchrvmasumlem1  27627  dchrvmasum2lem  27628  dchrvmasumlema  27632  dchrisum0flblem2  27641  dchrisum0fno1  27643  dchrisum0re  27645  logdivsum  27665  pntrsumbnd2  27699  pntpbnd1a  27717  pntpbnd1  27718  pntibndlem2  27723  pntlemr  27734  pntlemj  27735  pntlemf  27737  pnt2  27745  padicabv  27762  ostth2lem2  27766  lesrecd  27961  ltsrecd  27963  madebday  28061  addsproplem6  28135  negsproplem6  28194  mulsproplem13  28289  mulsproplem14  28290  ltmulsd  28298  mulsgt0d  28306  f1otrg  29163  brbtwn2  29198  colinearalglem2  29200  axcgrtr  29208  axcgrid  29209  axsegconlem7  29216  axsegcon  29220  ax5seglem3  29224  ax5seglem6  29227  ax5seg  29231  axpaschlem  29233  axlowdimlem17  29251  axcontlem2  29258  axcontlem4  29260  axcontlem7  29263  axcontlem8  29264  ecgrtg  29276  usgredg2v  29520  vtxdgoddnumeven  29846  2trlond  30231  eupthp1  30510  nmobndi  31070  ubthlem2  31166  ubthlem3  31167  minvecolem2  31170  shuni  31595  pjhthlem1  31686  chscllem2  31933  pjcompi  31967  mayete3i  32023  unoplin  32215  hmoplin  32237  nmophmi  32326  mdslmd4i  32628  isoun  32990  submuladdd  33028  receqid  33032  xrge0addcld  33050  xrofsup  33055  eliccelico  33065  elicoelioo  33066  difioo  33070  rexdiv  33188  mgcmnt1d  33260  mgcmnt2d  33261  xrge0addgt0  33280  cycpmcl  33379  cycpm2tr  33382  cyc3evpm  33413  cycpmconjslem2  33418  fldgensdrg  33580  qusker  33614  eqgvscpbl  33615  ringlsmss1  33653  ringlsmss2  33654  intlidl  33674  lidlunitel  33677  elrspunidl  33682  idlinsubrg  33685  mxidlmaxv  33698  mxidlprm  33700  ssmxidllem  33703  opprmxidlabs  33716  qsdrnglem2  33725  dflring3  33734  dflring4  33735  selvply1rhmlem4  33860  mplvrpmmhm  33883  mplvrpmrhm  33884  esplyind  33912  resssra  33924  ply1degltdimlem  33959  lindsunlem  33961  sdrgfldext  33987  fldsdrgfldext  33998  finexttrb  34002  fldgenfldext  34005  fldextrspunlem1  34012  algextdeglem4  34057  algextdeglem8  34061  constrextdg2lem  34085  mdetpmtr2  34161  mdetpmtr12  34162  madjusmdetlem1  34164  madjusmdetlem4  34167  rhmpreimacn  34222  unitdivcld  34238  xrge0mulc1cn  34278  qqhnm  34327  esumcst  34400  esumfsup  34407  esumpmono  34416  esumcvg  34423  difelsiga  34470  sigapisys  34492  sigapildsys  34499  ldgenpisyslem1  34500  1stmbfm  34597  2ndmbfm  34598  dya2icoseg  34614  sibfinima  34676  probmeasb  34767  orvcgteel  34805  orvclteel  34810  ballotlemsima  34853  ballotlemfrceq  34866  ccatmulgnn0dir  34879  fct2relem  34931  ftc2re  34932  chtvalz  34963  r1filimi  35442  subfacp1lem2a  35607  subfaclim  35615  erdsze2lem2  35631  cvmliftlem2  35713  cvmliftlem10  35721  cvmliftlem13  35723  cvmliftiota  35728  cvmlift2lem9  35738  cvmlift2lem11  35740  cvmlift2lem12  35741  cvmliftphtlem  35744  cvmlift3lem6  35751  cvmlift3lem7  35752  cvmlift3lem9  35754  snmlff  35756  mrsubfval  35935  wzel  36249  wsuclem  36250  brsegle  36535  opnregcld  36766  weiunfrlem  36900  fin2so  38183  poimirlem17  38213  poimirlem23  38219  opnmbllem0  38232  mblfinlem3  38235  mblfinlem4  38236  itg2addnclem  38247  itg2addnc  38250  itg2gt0cn  38251  ftc1cnnclem  38267  ftc1cnnc  38268  areacirclem5  38288  indexdom  38310  sstotbnd2  38350  isbnd3  38360  isbnd3b  38361  cntotbnd  38372  ismtyima  38379  heibor1lem  38385  heiborlem8  38394  rrncmslem  38408  reheibor  38415  lkrlsp  39803  lshpkrlem5  39815  ldualssvscl  39859  ldualssvsubcl  39860  llnmlplnN  40240  llncvrlpln  40259  pmapjat1  40554  pclfinN  40601  lautlt  40792  lauteq  40796  lautco  40798  ltrn11  40827  ltrnle  40830  ltrneq2  40849  cdlemednuN  41001  cdleme20k  41020  cdleme20l2  41022  cdleme20l  41023  cdleme20m  41024  cdleme21c  41028  cdleme22e  41045  cdleme22eALTN  41046  cdlemefrs32fva  41101  cdlemg4g  41317  cdlemg18b  41380  cdlemg18c  41381  cdlemj3  41524  dia2dimlem5  41769  dvhopN  41817  cdlemm10N  41819  dihjatcclem4  42122  dochexmidlem2  42162  lclkrlem2o  42222  lcfrlem5  42247  lcfrlem6  42248  lcdlssvscl  42307  mapdpglem6  42379  mapdpglem9  42381  mapdpglem12  42384  mapdpglem14  42386  mapdindp0  42420  hdmaprnlem7N  42556  hdmaprnlem8N  42557  hdmaprnlem3eN  42559  hgmapvvlem3  42626  dvun  43047  addinvcom  43120  mzpsubst  43408  eldioph2lem1  43420  eldioph2lem2  43421  eldioph2b  43423  diophin  43432  irrapxlem2  43479  irrapxlem4  43481  irrapxlem5  43482  pellexlem1  43485  pellexlem2  43486  pellexlem6  43490  elpell1qr2  43528  pell1qrgaplem  43529  pell1qrgap  43530  pellqrex  43535  pellfundex  43542  pellfund14  43554  rmspecsqrtnq  43562  rmxyadd  43577  congsub  43626  mzpcong  43628  congrep  43629  acongtr  43634  acongrep  43636  jm2.19lem1  43645  jm2.22  43651  jm2.23  43652  jm2.26lem3  43657  jm2.26  43658  jm2.27a  43661  fnwe2lem2  43707  aomclem6  43715  hbtlem2  43780  hbtlem4  43782  hbtlem5  43784  dgraa0p  43805  rngunsnply  43825  proot1hash  43851  nnoeomeqom  43968  cantnf2  43981  omabs2  43988  naddcnff  44018  naddcnffo  44020  naddcnfcom  44022  naddcnfid1  44023  expgrowth  44974  fpmd  45907  abslt2sqd  46005  ioondisj2  46138  ioondisj1  46139  eliocre  46154  ioossioobi  46162  iooiinicc  46187  iooiinioc  46201  lptioo2  46276  limcresiooub  46285  limsupequzlem  46365  xlimmnfvlem2  46476  xlimpnfvlem2  46480  cncfuni  46529  cncfiooicclem1  46536  cxpcncf2  46542  dvcnre  46559  dvresntr  46561  dvresioo  46564  dvbdfbdioolem1  46571  dvnmptdivc  46581  dvnxpaek  46585  itgsinexplem1  46597  itgcoscmulx  46612  itgiccshift  46623  itgperiod  46624  ovolsplit  46631  stoweidlem11  46654  stoweidlem26  46669  stoweidlem34  46677  stoweidlem36  46679  stoweidlem38  46681  stirlinglem5  46721  dirkercncflem2  46747  dirkercncflem4  46749  fourierdlem20  46770  fourierdlem58  46807  fourierdlem72  46821  fourierdlem73  46822  fourierdlem74  46823  fourierdlem75  46824  fourierdlem76  46825  fourierdlem79  46828  fourierdlem80  46829  fourierdlem87  46836  fourierdlem94  46843  fourierdlem103  46852  fourierdlem104  46853  fourierdlem107  46856  fourierdlem113  46862  sqwvfoura  46871  sqwvfourb  46872  fourierswlem  46873  fouriersw  46874  etransclem46  46923  etransclem47  46924  rrndistlt  46933  rrnprjdstle  46944  ioorrnopnxrlem  46949  sge0ssre  47040  sge0seq  47089  hsphoidmvle2  47228  hsphoidmvle  47229  hoidmv1lelem1  47234  hoidmv1lelem2  47235  hoidmv1lelem3  47236  hoidmvlelem1  47238  hoidifhspdmvle  47263  hoiqssbllem2  47266  ovolval5lem2  47296  iinhoiicc  47317  iunhoiioo  47319  vonioolem2  47324  vonicclem2  47327  issmflem  47370  submodlt  48019  iccpartdisj  48112  m1expevenALTV  48338  fpprel2  48432  tgoldbach  48508  opstrgric  48617  gpg3kgrtriex  48780  nn0eo  49230  fdivpm  49245  refdivpm  49246  elbigolo1  49259  logbpw2m1  49269  fllog2  49270  dignn0flhalflem1  49317  dignn0flhalflem2  49318  itsclinecirc0in  49477  2itscplem2  49481  itscnhlinecirc02plem1  49484  iccdisj2  49597