Theorem com12 33

Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 91. Its associated inference is mpi 21. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

Ref	Expression
com12.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
com12	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem com12

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2		com12.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5com 32	1 ⊢ (𝜓 → (𝜑 → 𝜒))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syl11  34  syl5  35  syl6com  38  mpcom  39  syli  40  syl2imc  42  pm2.27  43  syldc  49  pm2.43b  56  syl9r  79  com3r  88  pm2.86i  111  pm2.24  125  con3rr3  156  exptOLD  179  jad  189  pm2.61  194  syl5ibcom  248  syl5ibrcom  250  pm5.501  369  impcom  413  impd  416  expcom  419  expdcom  420  simplbi2com  508  imdistanri  580  syldbl2  855  jaod  873  orel1  902  pm2.62  913  pm2.75  947  pm2.64  956  ccased  1054  dedlem0b  1060  3impd  1367  3expd  1372  mp3an1i  1483  minimp  1653  meredith  1673  19.35  1909  speimfw  1995  equtrr  2054  equeucl  2056  ax12ev2  2215  sbiedw  2346  cbv1v  2365  exsb  2388  cbv1  2431  ax12b  2453  axc11n  2455  dvelimdf  2478  equvel  2485  dfsb1  2510  sbied  2532  dfmoeu  2560  mo3  2589  mo4  2591  2mo  2673  2eu6  2681  exists2  2686  pm2.61dne  3041  rexlimdv  3161  r19.21v  3187  r19.12  3311  2gencl  3492  3gencl  3493  vtocl2ga  3537  vtocl2gaf  3538  vtocl3gaf  3539  vtocl3ga  3540  vtocl4ga  3542  rspccv  3573  ceqex  3605  mob  3674  euind  3681  reuind  3710  2reu1  3844  sseq2  3934  nelss  3974  rexdifi  4086  reupick2  4276  disjeq0  4408  uneqdifeq  4447  sspw  4567  ssprsseq  4780  preq12b  4804  prnebg  4810  prel12g  4818  3elpr2eq  4833  iinss2  5015  trintss  5230  dtruALT2  5331  reusv2lem1  5359  alxfr  5368  ralxfrALT  5376  exexneq  5402  copsexgwOLD  5460  snopeqop  5477  propeqop  5478  opthhausdorff  5489  opthhausdorff0  5490  pofun  5576  solin  5585  frss  5614  2optocl  5746  3optocl  5747  ssrel  5758  ssrel2  5760  ssrelrel  5771  elrelb  5774  relop  5827  dfres3  5974  asymref2  6110  xpidtr  6115  trin2  6116  poltletr  6125  xp11  6166  imadifssranOLDOLD  6203  relcnvtrgOLD  6269  reuop  6296  tz7.7  6388  ordtr2  6408  suc11  6472  fundif  6589  fss  6726  f0dom0  6766  fv3  6903  tz6.12i  6911  mpteqb  7013  fveqdmss  7078  eldmrexrnb  7092  funopsnOLD  7152  funsndifnop  7155  tpres  7207  funfvima  7236  fvclss  7245  f1veqaeq  7260  fvf1pr  7315  isoselem  7349  oprabv  7480  ovg  7585  elovmpt3rab1  7681  sorpsscmpl  7750  iunpw  7785  trom  7886  limom  7893  peano5  7905  focdmex  7968  funelss  8058  funeldmdif  8059  bropopvvv  8101  bropfvvvvlem  8102  ovmptss  8104  f1o2ndf1  8135  poxp  8142  soxp  8143  poxp2  8162  frxp2  8163  frxp3  8170  suppimacnv  8194  ressuppss  8203  ressuppssdif  8205  tposfn2  8268  wfr3g  8340  onnseq  8355  smoel  8371  smogt  8378  smoiso2  8380  tfr3  8410  tz7.48-2  8455  tz7.48-3  8457  tz7.49  8458  oecl  8548  oaordex  8569  oalimcl  8571  oaass  8572  omordi  8577  omlimcl  8589  odi  8590  omeulem1  8593  oen0  8598  nnawordi  8633  nnaass  8634  nnmordi  8643  omabs  8663  omsmolem  8669  naddssim  8698  brinxper  8750  iiner  8813  2ecoptocl  8832  3ecoptocl  8833  undifixp  8965  xpdom2  9094  xpf1o  9161  infensuc  9177  findcard2  9183  php  9225  isinf  9259  unblem2  9288  fodomfir  9322  infssuni  9338  finsschain  9351  fsuppunfi  9383  fsuppunbi  9384  marypha1  9429  hartogs  9541  card2on  9551  card2inf  9552  xpwdomg  9582  elirrvOLD  9595  elirrvOLDOLD  9596  en3lp  9618  preleqg  9619  inf3lem1  9632  inf3lem2  9633  inf3lem3  9634  inf3lem5  9636  noinfep  9664  ttrclss  9724  ttrclselem2  9730  trcl  9732  tcel  9747  frr3g  9763  rankonidlem  9841  elhf4  9915  scottexOLD  9937  djuunxp  10005  eldju2ndl  10008  updjud  10018  dif1card  10092  fodomnum  10139  cardaleph  10171  kmlem9  10240  kmlem13  10244  cflim2  10344  cfsmolem  10351  infpssrlem3  10386  isfin7-2  10477  fin1a2lem6  10486  fin1a2lem12  10492  domtriomlem  10523  axdc3lem4  10534  axdc4lem  10536  zorn2lem3  10579  zorn2lem4  10580  zorn2lem5  10581  zorn2lem7  10583  zornn0g  10586  axdclem2  10601  ondomon  10650  alephval2  10660  cfpwsdom  10672  wuncval2  10835  grupr  10885  gruiun  10887  ingru  10903  grothomex  10917  indpi  10995  nqereu  11017  prlem934  11121  reclem2pr  11136  mulgt0sr  11193  supsrlem  11199  1re  11311  dedekind  11476  lemul1a  12174  squeeze0  12223  peano5nni  12341  nnadddir  12397  nnunb  12605  nn0lt2  12765  nn0le2is012  12766  fzind  12800  nn0ind-raph  12802  zindd  12803  uzin  13004  nn01to3  13071  xnn0xadd0  13380  xmulasslem  13418  icoshft  13607  fzen  13677  uzsubsubfz  13683  elfz0ubfz0  13769  elfz0fzfz0  13770  fz0fzelfz0  13771  elfzmlbp  13776  elfzodifsumelfzo  13869  ssfzo12bi  13899  fzoopth  13900  elfzonelfzo  13907  elfznelfzo  13911  injresinjlem  13928  injresinj  13929  modfzo0difsn  14089  modsumfzodifsn  14090  addmodlteq  14092  ssnn0fi  14131  fsuppmapnn0fiub0  14139  expcllem  14218  expeq0  14238  mulexp  14247  leexp2r  14320  bernneq  14376  facdiv  14434  hasheqf1oi  14498  hashnn0n0nn  14538  hashss  14556  hashgt12el  14570  hashgt12el2  14571  hashimarni  14589  hashle2pr  14625  pr2pwpr  14627  hashge2el2dif  14628  hashge2el2difr  14629  hashtpg  14633  hashge3el3dif  14635  exprelprel  14638  hash1to3  14640  hash3tpde  14641  tpfo  14648  fundmge2nop0  14650  fi1uzind  14655  ccatsymb  14731  swrdnd  14808  swrdnd2  14809  swrdnnn0nd  14810  swrdnd0  14811  pfxnd0  14842  swrdswrdlem  14857  swrdswrd  14858  pfxccatin12lem2a  14880  pfxccatin12lem1  14881  swrdccatin2  14882  pfxccatin12lem2  14884  pfxccatin12lem3  14885  pfxccat3  14887  swrdccat  14888  swrdccat3blem  14892  repsdf2  14933  repswswrd  14939  cshwidxmod  14958  cshwidx0  14961  cshf1  14965  cshweqrep  14976  cshw1  14977  2cshwcshw  14980  scshwfzeqfzo  14981  cshwcsh2id  14983  wwlktovfo  15116  relexpaddg  15211  iseraltlem2  15855  modfsummods  15965  clim2prod  16062  prodfn0  16068  prodfrec  16069  prodmo  16108  fprodabs  16146  binomfallfac  16212  fprodefsum  16266  dvdsaddre2b  16482  addmodlteqALT  16500  oddge22np1  16524  nn0enne  16552  nn0o1gt2  16556  sumeven  16562  sumodd  16563  dvdslegcd  16679  gcdneg  16699  dfgcd2  16724  rplpwr  16737  lcmf  16813  lcmftp  16816  lcmfunsnlem2lem1  16818  lcmfunsnlem2  16820  lcmfdvdsb  16823  coprmdvds1  16832  qredeq  16837  coprmprod  16841  coprmproddvdslem  16842  cncongr1  16847  cncongr2  16848  prm2orodd  16871  2mulprm  16873  nnnn0modprm0  16989  prm23lt5  16997  prm23ge5  16998  dvdsprmpweqnn  17068  dvdsprmpweqle  17069  oddprmdvds  17086  prmpwdvds  17087  prmreclem4  17102  ramcl  17212  prmgaplem6  17239  prmgaplem7  17240  prmgaplem8  17241  cshwshashlem1  17278  cshwshashlem2  17279  cshwshashlem3  17280  cshwrepswhash1  17285  setsn0fun  17356  setsstruct2  17357  imasleval  17718  mreiincl  17771  mreexexd  17827  inveq  17954  cicsym  17984  cictr  17985  initoid  18181  termoid  18182  initoeu2lem0  18193  initoeu2lem1  18194  initoeu2lem2  18195  initoeu2  18196  fthestrcsetc  18329  fthsetcestrc  18344  drsdirfi  18484  isnmgm  18825  mgmhmlin  18893  issubmgm2  18897  sgrpass  18919  insubm  19019  mgm2nsgrplem3  19124  dfgrp3lem  19253  cyccom  19423  symg2bas  19612  symgfix2  19635  symgextf1  19640  gsmsymgrfix  19647  pmtrprfv3  19673  psgnunilem4  19716  efgi2  19944  0ringnnzr  20781  rnghmsscmap  20887  rnghmsubcsetclem2  20889  rngcinv  20894  funcrngcsetc  20897  funcrngcsetcALT  20898  rhmsscmap  20916  rhmsubcsetclem2  20918  rhmsubcrngclem2  20924  ringcbasbas  20930  funcringcsetc  20931  rhmsubclem4  20945  unichnlidl  21521  rngqiprngimfo  21602  psgndiflemB  21911  psgndiflemA  21912  elfrlmbasn0  22074  lmictra  22156  mpfrcl  22399  gsummoncoe1  22631  mamufacex  22716  matecl  22745  dmatelnd  22816  dmatscmcl  22823  scmateALT  22832  scmatsgrp1  22842  scmatf1  22851  mavmulsolcl  22871  cramerimplem1  23006  cramerimplem2  23007  pmatcollpw3fi1  23111  mp2pm2mplem4  23132  pm2mpfo  23137  chmaidscmat  23171  fvmptnn04ifb  23174  chfacfscmul0  23181  chfacfpmmul0  23185  cayhamlem1  23189  cayhamlem3  23210  cayleyhamilton1  23215  fiinopn  23224  tgcl  23292  distop  23318  isclo2  23411  iscldtop  23418  ssnei2  23439  opnnei  23443  pnfnei  23543  mnfnei  23544  tgcnp  23576  cnpnei  23587  1stcelcls  23785  txcnpi  23932  cnmptcom  24002  fbfinnfr  24165  isfildlem  24181  snfil  24188  fbunfip  24193  fgcl  24202  elfm2  24272  fmco  24285  fbflim2  24301  cnpflf2  24324  flimfcls  24350  tmdgsum  24419  neibl  24825  tngngpim  24983  fgcfil  25597  caubl  25634  volsuplem  25881  ellimc3  26204  dvnadd  26254  dvnres  26256  cpnord  26260  dvnfre  26277  ply1divex  26460  plyconz  26636  cxpmul2  27022  fsumdvdsmul  27527  zabsle1  27628  gausslemma2dlem1a  27697  gausslemma2dlem3  27700  lgsquad2lem2  27717  2lgs  27739  2sq2  27765  2sqnn0  27770  2sqnn  27771  2sqreultlem  27779  2sqreunnltlem  27782  qabvexp  27958  ltsval2  28018  nolt02o  28057  sltsun1  28179  cutsun12  28181  madebday  28291  mulsprop  28521  precsexlem8  28605  precsexlem9  28606  noseqind  28683  om2noseqrdg  28695  n0cutlt  28750  peano5uzs  28795  expadds  28826  bdaypw2n0bndlem  28854  bdaypw2n0bnd  28855  axcontlem4  29550  umgredgprv  29690  umgrnloop  29691  upgrpredgv  29722  upgredgpr  29725  edglnl  29726  usgredgprvALT  29781  usgrnloopALT  29789  usgredg2v  29813  fusgrfis  29916  nbuhgr2vtx1edgblem  29937  nb3grprlem1  29966  cusgrsize2inds  30039  cusgrfi  30044  fusgrn0degnn0  30085  uspgrloopvtxel  30102  vtxdginducedm1lem4  30128  uhgr0edg0rgrb  30160  wlkl1loop  30223  wlk1walk  30224  upgriswlk  30226  upgrwlkvtxedg  30230  uspgr2wlkeq  30231  wlkv0  30235  wlksoneq1eq2  30248  wlkon2n0  30250  wlkreslem  30253  wlkres  30254  lfgrwlkprop  30275  pthdivtx  30317  2pthnloop  30322  spthonepeq  30343  uhgrwkspthlem2  30345  uhgrwkspth  30346  usgr2wlkneq  30347  usgr2trlncl  30351  usgr2pthlem  30354  usgr2pth  30355  cyclnspth  30394  spthcycl  30397  lfgrn1cycl  30399  usgr2trlncrct  30400  uspgrn2crct  30402  crctcshwlkn0lem3  30406  crctcshwlkn0lem5  30408  wwlknp  30437  wspthneq1eq2  30454  0enwwlksnge1  30458  wlklnwwlkln1  30462  wlkiswwlks2  30469  wlkiswwlksupgr2  30471  wlklnwwlkln2lem  30476  wwlksnred  30486  wwlksnextbi  30488  wwlksnredwwlkn0  30490  wwlksnextwrd  30491  wwlksnextinj  30493  wwlksnextproplem3  30505  wwlksnextprop  30506  wspthsnwspthsnon  30510  wspthsnonn0vne  30511  2pthon3v  30537  umgr2adedgwlkonALT  30541  umgr2wlk  30543  umgr2wlkon  30544  usgrwwlks2on  30552  umgrwwlks2on  30553  elwspths2on  30556  elwspths2onw  30557  usgr2wspthons3  30561  elwwlks2  30563  rusgrnumwwlk  30572  clwwlkccatlem  30585  clwlkclwwlklem2a4  30593  clwlkclwwlklem2a  30594  clwlkclwwlklem2  30596  clwlkclwwlkf1lem3  30602  erclwwlkeqlen  30615  clwwlknwwlksn  30634  loopclwwlkn1b  30638  clwwlkf1  30645  wwlksext2clwwlk  30653  eleclclwwlknlem2  30657  umgr2cwwk2dif  30660  eleclclwwlkn  30672  hashecclwwlkn1  30673  umgrhashecclwwlk  30674  clwwlknonwwlknonb  30702  clwwlknonex2lem2  30704  clwwlknonex2  30705  loop1cycl  30749  1pthon2v  30759  upgr3v3e3cycl  30786  uhgr3cyclexlem  30787  uhgr3cyclex  30788  eupth2lem3lem4  30837  frgr3vlem1  30879  frgr3vlem2  30880  3vfriswmgrlem  30883  3vfriswmgr  30884  3cyclfrgrrn1  30891  n4cyclfrgr  30897  frgrncvvdeqlem3  30907  frgrncvvdeqlem6  30910  frgrncvvdeqlem7  30911  frgrncvvdeqlem8  30912  frgrwopreglem4a  30916  frgrwopreglem3  30920  frgrwopreg1  30924  frgrwopreg2  30925  frgrwopreglem5lem  30926  frgrwopreglem5ALT  30928  frgrwopreg  30929  fusgr2wsp2nb  30940  2wspmdisj  30943  numclwwlk1lem2foa  30960  numclwwlk1lem2f1  30963  numclwwlk1lem2fo  30964  numclwwlk1  30967  wlkl0  30973  numclwwlk2lem1  30982  numclwlk2lem2f  30983  numclwlk2lem2f1o  30985  frgrreg  31000  frgrregord013  31001  frgrregord13  31002  friendshipgt3  31004  friendship  31005  eulplig  31092  ipassi  31448  ubthlem2  31478  isch3  31848  shintcli  31936  shmodsi  31996  spansncvi  32259  hoaddsub  32423  eigorthi  32444  pjss2coi  32771  pjnormssi  32775  pj3cor1i  32816  strb  32865  dmdmd  32907  mdsl0  32917  csmdsymi  32941  chrelat2i  32972  mdsymlem3  33012  mdsymlem6  33015  sumdmdlem2  33026  opreu2reuALT  33120  ssrelf  33256  gsumwun  33683  r1filim  35781  trssfir1om  35789  dfac16  35810  fineqvinfep  35849  trssfir1omregs  35860  karddom  35885  kardsdom  35886  kardexen  35887  j0ltaleph  35947  onvf1odlem4  35953  cvmlift2lem1  36153  satfrel  36218  satfrnmapom  36221  fmlafvel  36236  fmla1  36238  gonarlem  36245  gonar  36246  goalrlem  36247  goalr  36248  satffunlem  36252  satffunlem1lem1  36253  satffunlem2lem1  36255  satffun  36260  satefvfmla1  36276  mrsubvrs  36373  mclsax  36420  3ccased  36576  dfon2lem3  36639  rdgprc  36648  cgrextend  36865  btwndiff  36884  btwnconn1lem12  36955  brsegle  36965  broutsideof2  36979  funray  36997  in-ax8  37105  ss-ax8  37106  elicc3  37197  nn0prpwlem  37202  nn0prpw  37203  fnessref  37237  neibastop2lem  37240  filnetlem4  37261  meran1  37291  waj-ax  37294  arg-ax  37296  axtco1from2  37355  dfttc4  37410  mh-inf3f1  37421  mh-regprimbi  37425  bj-nnclavc  37505  bj-con2com  37522  bj-axdd2  37554  bj-alrimg  37575  bj-exlimg  37597  bj-exalimi  37607  bj-eximcom  37608  bj-ssbid1ALT  37656  bj-sb  37681  bj-snsetex  37968  bj-axseprep  38082  bj-axreprepsep  38083  bj-restpw  38105  bj-finsumval0  38299  mptsnunlem  38354  icoreclin  38373  relowlpssretop  38380  inunissunidif  38391  rdgssun  38394  finorwe  38398  domalom  38420  wl-dral1d  38556  wl-exeq  38559  wl-lem-exsb  38591  wl-eujustlem1  38613  poimirlem29  38660  poimirlem32  38663  findcard4  38725  fdc  38772  seqpo  38774  incsequz  38775  isismty  38828  ismtybndlem  38833  heibor1lem  38836  ismgmOLD  38877  isexid2  38882  ghomco  38918  pridlc  39098  relcnveq3  39352  elrelscnveq3  39652  cdleme18d  41445  tendovalco  41915  cdlemn11pre  42360  dihord2pre  42375  indstrd  43336  unitscyglem3  43340  eu6w  43780  incssnn0  43815  fphpd  43916  jm2.19lem3  44091  setindtr  44124  islssfg2  44166  mpaaeu  44245  ordnexbtwnsuc  44362  oaabsb  44389  succlg  44423  oacl2g  44425  omabs2  44427  omcl2  44428  omcl3g  44429  pr2cv  44642  refimssco  44700  iunrelexpmin1  44801  iunrelexpmin2  44805  trclimalb2  44819  clsk1indlem3  45136  tfindsd  45301  mnurndlem1  45358  nzss  45394  sb5ALT  45601  truniALT  45617  ee223  45710  3orbi123VD  45925  sbc3orgVD  45926  exbirVD  45928  exbiriVD  45929  sbcim2gVD  45950  trsbcVD  45952  truniALTVD  45953  onfrALTlem3VD  45962  onfrALTlem2VD  45964  csbrngVD  45971  19.41rgVD  45977  ax6e2eqVD  45982  ax6e2ndeqVD  45984  2uasbanhVD  45986  sb5ALTVD  45988  vk15.4jVD  45989  infxrunb3rnmpt  46531  stoweidlem26  47129  et-equeucl  47975  hirstL-ax3  48055  rexsb  48262  rexrsb  48263  euoreqb  48272  2reu8i  48276  afvres  48335  tz6.12-afv  48336  afvco2  48339  afv2orxorb  48391  afv2res  48402  tz6.12-afv2  48403  tz6.12i-afv2  48406  dfatcolem  48418  zm1nn  48465  2ffzoeq  48491  smonoord  48540  iccpartiltu  48597  iccpartlt  48599  iccpartltu  48600  iccpartgtl  48601  iccpartgt  48602  iccpartleu  48603  iccpartgel  48604  icceuelpart  48611  iccpartnel  48613  lswn0  48619  ichnreuop  48647  ichreuopeq  48648  prsprel  48662  sprsymrelfvlem  48665  sprsymrelf1lem  48666  sprsymrelfolem2  48668  prproropf1olem4  48681  paireqne  48686  prprelb  48691  reupr  48697  goldbachth  48725  odz2prm2pw  48741  fmtno4prmfac  48750  fmtno4prmfac193  48751  prmdvdsfmtnof1lem2  48763  2pwp1prmfmtno  48768  lighneallem2  48784  lighneallem4b  48787  lighneallem4  48788  requad2  48814  odd2prm2  48909  mogoldbblem  48911  gbepos  48949  gbowgt5  48953  gbowge7  48954  stgoldbwt  48967  sbgoldbwt  48968  sbgoldbst  48969  sbgoldbaltlem1  48970  sbgoldbalt  48972  sbgoldbo  48978  nnsum3primesle9  48985  nnsum4primesodd  48987  nnsum4primesoddALTV  48988  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  bgoldbtbndlem1  48996  bgoldbtbndlem2  48997  bgoldbtbndlem3  48998  bgoldbtbnd  49000  dfnbgr6  49048  isuspgrimlem  49086  uhgrimisgrgric  49122  clnbgrgrim  49125  usgrgrtrirex  49141  isubgr3stgrlem4  49160  grilcbri2  49202  grlicsym  49204  grlictr  49206  gricgrlic  49209  gpgvtxedg0  49254  gpgvtxedg1  49255  gpgedg2ov  49257  gpgedg2iv  49258  pgnioedg1  49299  pgnioedg2  49300  pgnioedg3  49301  pgnioedg4  49302  pgnioedg5  49303  pgnbgreunbgrlem2lem3  49307  pgnbgreunbgrlem3  49309  pgnbgreunbgrlem5lem1  49311  pgnbgreunbgrlem5lem2  49312  pgnbgreunbgrlem5lem3  49313  pgnbgreunbgrlem6  49315  upgrwlkupwlk  49331  uspgrsprf1  49338  lmod0rng  49419  lidldomn1  49421  rngccatidALTV  49462  rngcinvALTV  49466  rhmsubcALTVlem4  49474  funcringcsetcALTV2lem9  49488  ringccatidALTV  49496  ringcbasbasALTV  49502  ztprmneprm  49552  pgrpgt2nabl  49571  lmodvsmdi  49584  ply1mulgsumlem2  49592  lincsumcl  49636  ellcoellss  49640  linindslinci  49653  islinindfis  49654  lincext3  49661  lindslinindimp2lem4  49666  lindslinindsimp2lem5  49667  lindslinindsimp2  49668  lindsrng01  49673  ldepspr  49678  lincresunit3lem1  49684  elfzolborelfzop1  49724  dignn0ldlem  49807  nn0sumshdiglem1  49826  1arymaptf1  49847  2arymaptf1  49858  rrx2plord2  49928  rrx2plordisom  49929  line2ylem  49956  line2xlem  49958  line2y  49960  itschlc0xyqsol1  49971  inlinecirc02plem  49991  fullthinc  50678  tfis2d  50955  onsetrec  50969