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  1484  minimp  1654  meredith  1674  19.35  1912  speimfw  1998  equtrr  2057  equeucl  2059  nf5di  2184  ax12ev2  2219  sbiedw  2350  cbv1v  2369  exsb  2391  cbv1  2434  ax12b  2456  axc11n  2458  dvelimdf  2481  equvel  2488  dfsb1  2513  sbied  2535  dfmoeu  2563  mo3  2592  mo4  2594  2mo  2676  2eu6  2684  exists2  2689  pm2.61dne  3045  rexlimdv  3165  r19.21v  3191  r19.12  3315  2gencl  3496  3gencl  3497  vtocl2ga  3541  vtocl2gaf  3542  vtocl3gaf  3543  vtocl3ga  3544  vtocl4ga  3546  rspccv  3577  ceqex  3609  mob  3678  euind  3685  reuind  3714  2reu1  3849  sseq2  3939  nelss  3979  rexdifi  4089  reupick2  4279  disjeq0  4412  uneqdifeq  4451  sspw  4571  ssprsseq  4784  preq12b  4808  prnebg  4814  prel12g  4822  3elpr2eq  4837  iinss2  5019  trintss  5234  dtruALT2  5336  reusv2lem1  5364  alxfr  5373  ralxfrALT  5381  exexneq  5407  copsexgwOLD  5465  snopeqop  5482  propeqop  5483  opthhausdorff  5494  opthhausdorff0  5495  pofun  5581  solin  5590  frss  5619  2optocl  5752  3optocl  5753  ssrel  5764  ssrel2  5766  ssrelrel  5777  elrelb  5780  relop  5834  dfres3  5986  asymref2  6123  xpidtr  6128  trin2  6129  poltletr  6138  xp11  6179  imadifssranOLDOLD  6216  relcnvtrgOLD  6287  reuop  6314  tz7.7  6406  ordtr2  6426  suc11  6490  fundifOLD  6611  fss  6748  f0dom0  6788  fv3  6926  tz6.12i  6934  mpteqb  7036  fveqdmss  7102  eldmrexrnb  7116  funopsnOLD  7176  funsndifnop  7179  tpres  7230  funfvima  7259  fvclss  7268  f1veqaeq  7283  fvf1pr  7338  isoselem  7372  oprabv  7503  ovg  7609  elovmpt3rab1  7705  sorpsscmpl  7774  iunpw  7809  trom  7910  limom  7917  peano5  7929  focdmex  7992  funelss  8083  funeldmdif  8084  bropopvvv  8126  bropfvvvvlem  8127  ovmptss  8129  f1o2ndf1  8160  poxp  8167  soxp  8168  poxp2  8187  frxp2  8188  frxp3  8195  suppimacnv  8219  ressuppss  8228  ressuppssdif  8230  tposfn2  8293  wfr3g  8365  onnseq  8380  smoel  8396  smogt  8403  smoiso2  8405  tfr3  8435  tz7.48-2  8480  tz7.48-3  8482  tz7.49  8483  oecl  8573  oaordex  8594  oalimcl  8596  oaass  8597  omordi  8602  omlimcl  8614  odi  8615  omeulem1  8618  oen0  8623  nnawordi  8658  nnaass  8659  nnmordi  8668  omabs  8688  omsmolem  8694  naddssim  8723  brinxper  8775  iiner  8838  2ecoptocl  8857  3ecoptocl  8858  undifixp  8990  xpdom2  9119  xpf1o  9186  infensuc  9202  findcard2  9208  php  9250  isinf  9284  unblem2  9313  fodomfir  9347  infssuni  9363  finsschain  9376  fsuppunfi  9407  fsuppunbi  9408  marypha1  9453  hartogs  9565  card2on  9575  card2inf  9576  xpwdomg  9606  elirrvOLD  9619  elirrvOLDOLD  9620  en3lp  9642  preleqg  9643  inf3lem1  9656  inf3lem2  9657  inf3lem3  9658  inf3lem5  9660  noinfep  9688  ttrclss  9748  ttrclselem2  9754  trcl  9756  tcel  9771  frr3g  9787  rankonidlem  9865  elhf4  9939  scottexOLD  9961  djuunxp  10029  eldju2ndl  10032  updjud  10042  dif1card  10116  fodomnum  10163  cardaleph  10195  kmlem9  10264  kmlem13  10268  cflim2  10368  cfsmolem  10375  infpssrlem3  10410  isfin7-2  10501  fin1a2lem6  10510  fin1a2lem12  10516  domtriomlem  10547  axdc3lem4  10558  axdc4lem  10560  zorn2lem3  10603  zorn2lem4  10604  zorn2lem5  10605  zorn2lem7  10607  zornn0g  10610  axdclem2  10625  ondomon  10674  alephval2  10684  cfpwsdom  10696  wuncval2  10859  grupr  10909  gruiun  10911  ingru  10927  grothomex  10941  indpi  11019  nqereu  11041  prlem934  11145  reclem2pr  11160  mulgt0sr  11217  supsrlem  11223  1re  11335  dedekind  11500  lemul1a  12198  squeeze0  12247  peano5nni  12365  nnadddir  12421  nnunb  12629  nn0lt2  12789  nn0le2is012  12790  fzind  12824  nn0ind-raph  12826  zindd  12827  uzin  13028  nn01to3  13095  xnn0xadd0  13404  xmulasslem  13442  icoshft  13631  fzen  13701  uzsubsubfz  13707  elfz0ubfz0  13793  elfz0fzfz0  13794  fz0fzelfz0  13795  elfzmlbp  13800  elfzodifsumelfzo  13893  ssfzo12bi  13923  fzoopth  13924  elfzonelfzo  13931  elfznelfzo  13935  injresinjlem  13952  injresinj  13953  modfzo0difsn  14113  modsumfzodifsn  14114  addmodlteq  14116  ssnn0fi  14155  fsuppmapnn0fiub0  14163  expcllem  14242  expeq0  14262  mulexp  14271  leexp2r  14344  bernneq  14400  facdiv  14458  hasheqf1oi  14522  hashnn0n0nn  14562  hashss  14580  hashgt12el  14594  hashgt12el2  14595  hashimarni  14613  hashle2pr  14649  pr2pwpr  14651  hashge2el2dif  14652  hashge2el2difr  14653  hashtpg  14657  hashge3el3dif  14659  exprelprel  14662  hash1to3  14664  hash3tpde  14665  tpfo  14672  fundmge2nop0  14674  fi1uzind  14679  ccatsymb  14755  swrdnd  14832  swrdnd2  14833  swrdnnn0nd  14834  swrdnd0  14835  pfxnd0  14866  swrdswrdlem  14881  swrdswrd  14882  pfxccatin12lem2a  14904  pfxccatin12lem1  14905  swrdccatin2  14906  pfxccatin12lem2  14908  pfxccatin12lem3  14909  pfxccat3  14911  swrdccat  14912  swrdccat3blem  14916  repsdf2  14957  repswswrd  14963  cshwidxmod  14982  cshwidx0  14985  cshf1  14989  cshweqrep  15000  cshw1  15001  2cshwcshw  15004  scshwfzeqfzo  15005  cshwcsh2id  15007  wwlktovfo  15140  relexpaddg  15235  iseraltlem2  15879  modfsummods  15989  clim2prod  16086  prodfn0  16092  prodfrec  16093  prodmo  16132  fprodabs  16170  binomfallfac  16236  fprodefsum  16290  dvdsaddre2b  16506  addmodlteqALT  16524  oddge22np1  16548  nn0enne  16576  nn0o1gt2  16580  sumeven  16586  sumodd  16587  dvdslegcd  16703  gcdneg  16723  dfgcd2  16748  rplpwr  16761  lcmf  16837  lcmftp  16840  lcmfunsnlem2lem1  16842  lcmfunsnlem2  16844  lcmfdvdsb  16847  coprmdvds1  16856  qredeq  16861  coprmprod  16865  coprmproddvdslem  16866  cncongr1  16871  cncongr2  16872  prm2orodd  16895  2mulprm  16897  nnnn0modprm0  17013  prm23lt5  17021  prm23ge5  17022  dvdsprmpweqnn  17092  dvdsprmpweqle  17093  oddprmdvds  17110  prmpwdvds  17111  prmreclem4  17126  ramcl  17236  prmgaplem6  17263  prmgaplem7  17264  prmgaplem8  17265  cshwshashlem1  17302  cshwshashlem2  17303  cshwshashlem3  17304  cshwrepswhash1  17309  setsn0fun  17380  setsstruct2  17381  imasleval  17742  mreiincl  17795  mreexexd  17851  inveq  17978  cicsym  18008  cictr  18009  initoid  18205  termoid  18206  initoeu2lem0  18217  initoeu2lem1  18218  initoeu2lem2  18219  initoeu2  18220  fthestrcsetc  18353  fthsetcestrc  18368  drsdirfi  18508  isnmgm  18849  mgmhmlin  18917  issubmgm2  18921  sgrpass  18943  insubm  19043  mgm2nsgrplem3  19148  dfgrp3lem  19277  cyccom  19447  symg2bas  19637  symgfix2  19660  symgextf1  19665  gsmsymgrfix  19672  pmtrprfv3  19698  psgnunilem4  19741  efgi2  19969  0ringnnzr  20806  rnghmsscmap  20912  rnghmsubcsetclem2  20914  rngcinv  20919  funcrngcsetc  20922  funcrngcsetcALT  20923  rhmsscmap  20941  rhmsubcsetclem2  20943  rhmsubcrngclem2  20949  ringcbasbas  20955  funcringcsetc  20956  rhmsubclem4  20970  unichnlidl  21546  rngqiprngimfo  21627  psgndiflemB  21936  psgndiflemA  21937  elfrlmbasn0  22099  lmictra  22181  mpfrcl  22424  gsummoncoe1  22656  mamufacex  22741  matecl  22770  dmatelnd  22841  dmatscmcl  22848  scmateALT  22857  scmatsgrp1  22867  scmatf1  22876  mavmulsolcl  22896  cramerimplem1  23031  cramerimplem2  23032  pmatcollpw3fi1  23136  mp2pm2mplem4  23157  pm2mpfo  23162  chmaidscmat  23196  fvmptnn04ifb  23199  chfacfscmul0  23206  chfacfpmmul0  23210  cayhamlem1  23214  cayhamlem3  23235  cayleyhamilton1  23240  fiinopn  23249  tgcl  23317  distop  23343  isclo2  23436  iscldtop  23443  ssnei2  23464  opnnei  23468  pnfnei  23568  mnfnei  23569  tgcnp  23601  cnpnei  23612  1stcelcls  23810  txcnpi  23957  cnmptcom  24027  fbfinnfr  24190  isfildlem  24206  snfil  24213  fbunfip  24218  fgcl  24227  elfm2  24297  fmco  24310  fbflim2  24326  cnpflf2  24349  flimfcls  24375  tmdgsum  24444  neibl  24850  tngngpim  25008  fgcfil  25622  caubl  25659  volsuplem  25906  ellimc3  26229  dvnadd  26279  dvnres  26281  cpnord  26285  dvnfre  26302  ply1divex  26485  plyconz  26661  cxpmul2  27047  fsumdvdsmul  27552  zabsle1  27653  gausslemma2dlem1a  27722  gausslemma2dlem3  27725  lgsquad2lem2  27742  2lgs  27764  2sq2  27790  2sqnn0  27795  2sqnn  27796  2sqreultlem  27804  2sqreunnltlem  27807  qabvexp  27983  ltsval2  28043  nolt02o  28082  sltsun1  28204  cutsun12  28206  madebday  28316  mulsprop  28546  precsexlem8  28630  precsexlem9  28631  noseqind  28708  om2noseqrdg  28720  n0cutlt  28775  peano5uzs  28820  expadds  28851  bdaypw2n0bndlem  28879  bdaypw2n0bnd  28880  axcontlem4  29575  umgredgprv  29715  umgrnloop  29716  upgrpredgv  29747  upgredgpr  29750  edglnl  29751  usgredgprvALT  29806  usgrnloopALT  29814  usgredg2v  29838  fusgrfis  29941  nbuhgr2vtx1edgblem  29962  nb3grprlem1  29991  cusgrsize2inds  30064  cusgrfi  30069  fusgrn0degnn0  30110  uspgrloopvtxel  30127  vtxdginducedm1lem4  30153  uhgr0edg0rgrb  30185  wlkl1loop  30248  wlk1walk  30249  upgriswlk  30251  upgrwlkvtxedg  30255  uspgr2wlkeq  30256  wlkv0  30260  wlksoneq1eq2  30273  wlkon2n0  30275  wlkreslem  30278  wlkres  30279  lfgrwlkprop  30300  pthdivtx  30342  2pthnloop  30347  spthonepeq  30368  uhgrwkspthlem2  30370  uhgrwkspth  30371  usgr2wlkneq  30372  usgr2trlncl  30376  usgr2pthlem  30379  usgr2pth  30380  cyclnspth  30419  spthcycl  30422  lfgrn1cycl  30424  usgr2trlncrct  30425  uspgrn2crct  30427  crctcshwlkn0lem3  30431  crctcshwlkn0lem5  30433  wwlknp  30462  wspthneq1eq2  30479  0enwwlksnge1  30483  wlklnwwlkln1  30487  wlkiswwlks2  30494  wlkiswwlksupgr2  30496  wlklnwwlkln2lem  30501  wwlksnred  30511  wwlksnextbi  30513  wwlksnredwwlkn0  30515  wwlksnextwrd  30516  wwlksnextinj  30518  wwlksnextproplem3  30530  wwlksnextprop  30531  wspthsnwspthsnon  30535  wspthsnonn0vne  30536  2pthon3v  30562  umgr2adedgwlkonALT  30566  umgr2wlk  30568  umgr2wlkon  30569  usgrwwlks2on  30577  umgrwwlks2on  30578  elwspths2on  30581  elwspths2onw  30582  usgr2wspthons3  30586  elwwlks2  30588  rusgrnumwwlk  30597  clwwlkccatlem  30610  clwlkclwwlklem2a4  30618  clwlkclwwlklem2a  30619  clwlkclwwlklem2  30621  clwlkclwwlkf1lem3  30627  erclwwlkeqlen  30640  clwwlknwwlksn  30659  loopclwwlkn1b  30663  clwwlkf1  30670  wwlksext2clwwlk  30678  eleclclwwlknlem2  30682  umgr2cwwk2dif  30685  eleclclwwlkn  30697  hashecclwwlkn1  30698  umgrhashecclwwlk  30699  clwwlknonwwlknonb  30727  clwwlknonex2lem2  30729  clwwlknonex2  30730  loop1cycl  30774  1pthon2v  30784  upgr3v3e3cycl  30811  uhgr3cyclexlem  30812  uhgr3cyclex  30813  eupth2lem3lem4  30862  frgr3vlem1  30904  frgr3vlem2  30905  3vfriswmgrlem  30908  3vfriswmgr  30909  3cyclfrgrrn1  30916  n4cyclfrgr  30922  frgrncvvdeqlem3  30932  frgrncvvdeqlem6  30935  frgrncvvdeqlem7  30936  frgrncvvdeqlem8  30937  frgrwopreglem4a  30941  frgrwopreglem3  30945  frgrwopreg1  30949  frgrwopreg2  30950  frgrwopreglem5lem  30951  frgrwopreglem5ALT  30953  frgrwopreg  30954  fusgr2wsp2nb  30965  2wspmdisj  30968  numclwwlk1lem2foa  30985  numclwwlk1lem2f1  30988  numclwwlk1lem2fo  30989  numclwwlk1  30992  wlkl0  30998  numclwwlk2lem1  31007  numclwlk2lem2f  31008  numclwlk2lem2f1o  31010  frgrreg  31025  frgrregord013  31026  frgrregord13  31027  friendshipgt3  31029  friendship  31030  eulplig  31117  ipassi  31473  ubthlem2  31503  isch3  31873  shintcli  31961  shmodsi  32021  spansncvi  32284  hoaddsub  32448  eigorthi  32469  pjss2coi  32796  pjnormssi  32800  pj3cor1i  32841  strb  32890  dmdmd  32932  mdsl0  32942  csmdsymi  32966  chrelat2i  32997  mdsymlem3  33037  mdsymlem6  33040  sumdmdlem2  33051  opreu2reuALT  33145  ssrelf  33281  gsumwun  33707  r1filim  35813  trssfihf  35819  dfac16  35846  fineqvinfep  35893  trssfihfregs  35904  karddom  35929  kardsdom  35930  kardexen  35931  j0ltaleph  36008  onvf1odlem4  36034  cvmlift2lem1  36234  satfrel  36299  satfrnmapom  36302  fmlafvel  36317  fmla1  36319  gonarlem  36326  gonar  36327  goalrlem  36328  goalr  36329  satffunlem  36333  satffunlem1lem1  36334  satffunlem2lem1  36336  satffun  36341  satefvfmla1  36357  mrsubvrs  36454  mclsax  36501  elpssmo  36636  3ccased  36662  dfon2lem3  36725  rdgprc  36734  cgrextend  36951  btwndiff  36970  btwnconn1lem12  37041  brsegle  37051  broutsideof2  37065  funray  37083  in-ax8  37191  ss-ax8  37192  elicc3  37283  nn0prpwlem  37288  nn0prpw  37289  fnessref  37323  neibastop2lem  37326  filnetlem4  37347  meran1  37377  waj-ax  37380  arg-ax  37382  axtco1from2  37441  dfttc4  37496  mh-inf3f1  37507  mh-regprimbi  37511  bj-nnclavc  37591  bj-con2com  37608  bj-axdd2  37640  bj-alrimg  37661  bj-exlimg  37683  bj-exalimi  37693  bj-eximcom  37694  bj-ssbid1ALT  37742  bj-sb  37767  bj-snsetex  38054  bj-axseprep  38181  bj-axreprepsep  38182  bj-restpw  38204  bj-finsumval0  38398  mptsnunlem  38453  icoreclin  38472  relowlpssretop  38479  inunissunidif  38490  rdgssun  38493  finorwe  38497  domalom  38519  wl-dral1d  38655  wl-exeq  38658  wl-lem-exsb  38690  wl-eujustlem1  38712  poimirlem29  38759  poimirlem32  38762  findcard4  38824  fdc  38871  seqpo  38873  incsequz  38874  isismty  38927  ismtybndlem  38932  heibor1lem  38935  ismgmOLD  38976  isexid2  38981  ghomco  39017  pridlc  39197  relcnveq3  39451  elrelscnveq3  39751  cdleme18d  41544  tendovalco  42014  cdlemn11pre  42459  dihord2pre  42474  indstrd  43435  unitscyglem3  43439  eu6w  43880  incssnn0  43915  fphpd  44016  jm2.19lem3  44191  setindtr  44224  islssfg2  44266  mpaaeu  44344  ordnexbtwnsuc  44461  oaabsb  44488  succlg  44522  oacl2g  44524  omabs2  44526  omcl2  44527  omcl3g  44528  pr2cv  44741  refimssco  44799  iunrelexpmin1  44900  iunrelexpmin2  44904  trclimalb2  44918  clsk1indlem3  45235  tfindsd  45400  mnurndlem1  45457  nzss  45493  sb5ALT  45699  truniALT  45715  ee223  45808  3orbi123VD  46023  sbc3orgVD  46024  exbirVD  46026  exbiriVD  46027  sbcim2gVD  46048  trsbcVD  46050  truniALTVD  46051  onfrALTlem3VD  46060  onfrALTlem2VD  46062  csbrngVD  46069  19.41rgVD  46075  ax6e2eqVD  46080  ax6e2ndeqVD  46082  2uasbanhVD  46084  sb5ALTVD  46086  vk15.4jVD  46087  infxrunb3rnmpt  46643  stoweidlem26  47241  et-equeucl  48087  hirstL-ax3  48167  rexsb  48375  rexrsb  48376  euoreqb  48385  2reu8i  48389  afvres  48447  tz6.12-afv  48448  afvco2  48451  afv2orxorb  48503  afv2res  48514  tz6.12-afv2  48515  tz6.12i-afv2  48518  dfatcolem  48530  zm1nn  48577  2ffzoeq  48603  smonoord  48652  iccpartiltu  48709  iccpartlt  48711  iccpartltu  48712  iccpartgtl  48713  iccpartgt  48714  iccpartleu  48715  iccpartgel  48716  icceuelpart  48723  iccpartnel  48725  lswn0  48731  ichnreuop  48759  ichreuopeq  48760  prsprel  48774  sprsymrelfvlem  48777  sprsymrelf1lem  48778  sprsymrelfolem2  48780  prproropf1olem4  48793  paireqne  48798  prprelb  48803  reupr  48809  goldbachth  48837  odz2prm2pw  48853  fmtno4prmfac  48862  fmtno4prmfac193  48863  prmdvdsfmtnof1lem2  48875  2pwp1prmfmtno  48880  lighneallem2  48896  lighneallem4b  48899  lighneallem4  48900  requad2  48926  odd2prm2  49021  mogoldbblem  49023  gbepos  49061  gbowgt5  49065  gbowge7  49066  stgoldbwt  49079  sbgoldbwt  49080  sbgoldbst  49081  sbgoldbaltlem1  49082  sbgoldbalt  49084  sbgoldbo  49090  nnsum3primesle9  49097  nnsum4primesodd  49099  nnsum4primesoddALTV  49100  nnsum4primeseven  49103  nnsum4primesevenALTV  49104  bgoldbtbndlem1  49108  bgoldbtbndlem2  49109  bgoldbtbndlem3  49110  bgoldbtbnd  49112  dfnbgr6  49160  isuspgrimlem  49198  uhgrimisgrgric  49234  clnbgrgrim  49237  usgrgrtrirex  49253  isubgr3stgrlem4  49272  grilcbri2  49314  grlicsym  49316  grlictr  49318  gricgrlic  49321  gpgvtxedg0  49366  gpgvtxedg1  49367  gpgedg2ov  49369  gpgedg2iv  49370  pgnioedg1  49411  pgnioedg2  49412  pgnioedg3  49413  pgnioedg4  49414  pgnioedg5  49415  pgnbgreunbgrlem2lem3  49419  pgnbgreunbgrlem3  49421  pgnbgreunbgrlem5lem1  49423  pgnbgreunbgrlem5lem2  49424  pgnbgreunbgrlem5lem3  49425  pgnbgreunbgrlem6  49427  upgrwlkupwlk  49443  uspgrsprf1  49450  lmod0rng  49531  lidldomn1  49533  rngccatidALTV  49574  rngcinvALTV  49578  rhmsubcALTVlem4  49586  funcringcsetcALTV2lem9  49600  ringccatidALTV  49608  ringcbasbasALTV  49614  ztprmneprm  49664  pgrpgt2nabl  49683  lmodvsmdi  49696  ply1mulgsumlem2  49704  lincsumcl  49748  ellcoellss  49752  linindslinci  49765  islinindfis  49766  lincext3  49773  lindslinindimp2lem4  49778  lindslinindsimp2lem5  49779  lindslinindsimp2  49780  lindsrng01  49785  ldepspr  49790  lincresunit3lem1  49796  elfzolborelfzop1  49836  dignn0ldlem  49919  nn0sumshdiglem1  49938  1arymaptf1  49959  2arymaptf1  49970  rrx2plord2  50040  rrx2plordisom  50041  line2ylem  50068  line2xlem  50070  line2y  50072  itschlc0xyqsol1  50083  inlinecirc02plem  50103  fullthinc  50790  tfis2d  51067  onsetrec  51081