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  1654  meredith  1674  19.35  1910  speimfw  1996  equtrr  2055  equeucl  2057  ax12ev2  2218  sbiedw  2348  cbv1v  2367  exsb  2390  cbv1  2433  ax12b  2455  axc11n  2457  dvelimdf  2480  equvel  2487  dfsb1  2512  sbied  2534  dfmoeu  2562  mo3  2591  mo4  2593  2mo  2675  2eu6  2683  exists2  2688  pm2.61dne  3043  rexlimdv  3163  r19.21v  3189  r19.12  3313  2gencl  3495  3gencl  3496  vtocl2ga  3540  vtocl2gaf  3541  vtocl3gaf  3542  vtocl3ga  3543  vtocl4ga  3545  rspccv  3576  ceqex  3609  mob  3678  euind  3685  reuind  3714  2reu1  3848  sseq2  3960  nelss  4000  rexdifi  4100  reupick2  4280  disjeq0  4412  uneqdifeq  4451  sspw  4571  ssprsseq  4789  preq12b  4813  prnebg  4819  prel12g  4827  3elpr2eq  4869  iinss2  5020  trintss  5235  dtruALT2  5339  reusv2lem1  5367  alxfr  5376  ralxfrALT  5384  exexneq  5414  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  snopeqop  5487  propeqop  5488  opthhausdorff  5498  opthhausdorff0  5499  pofun  5585  solin  5594  frss  5623  2optocl  5755  3optocl  5756  ssrel  5767  ssrel2  5769  ssrelrel  5780  relop  5834  dfres3  5981  asymref2  6115  xpidtr  6120  trin2  6121  poltletr  6130  xp11  6172  imadifssranOLD  6202  relcnvtrgOLD  6268  reuop  6295  tz7.7  6387  ordtr2  6407  suc11  6471  fundif  6586  fss  6723  f0dom0  6763  fv3  6900  tz6.12i  6908  mpteqb  7010  fveqdmss  7075  eldmrexrnb  7089  funopsnOLD  7149  funsndifnop  7152  tpres  7204  funfvima  7233  fvclss  7242  f1veqaeq  7257  fvf1pr  7312  isoselem  7346  oprabv  7477  ovg  7582  elovmpt3rab1  7678  sorpsscmpl  7739  iunpw  7774  trom  7875  limom  7882  peano5  7894  focdmex  7957  funelss  8048  funeldmdif  8049  bropopvvv  8091  bropfvvvvlem  8092  f1o2ndf1  8123  poxp  8130  soxp  8131  poxp2  8145  frxp2  8146  frxp3  8153  suppimacnv  8176  ressuppss  8185  ressuppssdif  8187  tposfn2  8250  wfr3g  8322  onnseq  8337  smoel  8353  smogt  8360  smoiso2  8362  tfr3  8392  tz7.48-2  8435  tz7.48-3  8437  tz7.49  8438  oecl  8528  oaordex  8549  oalimcl  8551  oaass  8552  omordi  8557  omlimcl  8569  odi  8570  omeulem1  8573  oen0  8578  nnawordi  8613  nnaass  8614  nnmordi  8623  omabs  8643  omsmolem  8649  naddssim  8678  brinxper  8730  iiner  8793  2ecoptocl  8812  3ecoptocl  8813  undifixp  8945  xpdom2  9074  xpf1o  9141  infensuc  9157  findcard2  9163  php  9205  isinf  9239  unblem2  9267  fodomfir  9301  infssuni  9317  finsschain  9330  fsuppunfi  9362  fsuppunbi  9363  marypha1  9408  hartogs  9520  card2on  9530  card2inf  9531  xpwdomg  9561  elirrvOLD  9574  elirrvOLDOLD  9575  en3lp  9597  preleqg  9598  inf3lem1  9611  inf3lem2  9612  inf3lem3  9613  inf3lem5  9615  noinfep  9643  ttrclss  9703  ttrclselem2  9709  trcl  9711  tcel  9726  frr3g  9742  rankonidlem  9814  scottexOLD  9877  djuunxp  9930  eldju2ndl  9933  updjud  9943  dif1card  10017  fodomnum  10064  cardaleph  10096  kmlem9  10165  kmlem13  10169  cflim2  10269  cfsmolem  10276  infpssrlem3  10311  isfin7-2  10402  fin1a2lem6  10411  fin1a2lem12  10417  domtriomlem  10448  axdc3lem4  10459  axdc4lem  10461  zorn2lem3  10504  zorn2lem4  10505  zorn2lem5  10506  zorn2lem7  10508  zornn0g  10511  axdclem2  10526  ondomon  10575  alephval2  10585  cfpwsdom  10597  wuncval2  10760  grupr  10810  gruiun  10812  ingru  10828  grothomex  10842  indpi  10920  nqereu  10942  prlem934  11046  reclem2pr  11061  mulgt0sr  11118  supsrlem  11124  1re  11236  dedekind  11401  lemul1a  12097  squeeze0  12146  peano5nni  12264  nnadddir  12320  nnunb  12528  nn0lt2  12688  nn0le2is012  12689  fzind  12723  nn0ind-raph  12725  zindd  12726  uzin  12927  nn01to3  12994  xnn0xadd0  13303  xmulasslem  13341  icoshft  13530  fzen  13599  uzsubsubfz  13605  elfz0ubfz0  13691  elfz0fzfz0  13692  fz0fzelfz0  13693  elfzmlbp  13698  elfzodifsumelfzo  13791  ssfzo12bi  13821  fzoopth  13822  elfzonelfzo  13829  elfznelfzo  13833  injresinjlem  13850  injresinj  13851  modfzo0difsn  14011  modsumfzodifsn  14012  addmodlteq  14014  ssnn0fi  14053  fsuppmapnn0fiub0  14061  expcllem  14140  expeq0  14160  mulexp  14169  leexp2r  14242  bernneq  14297  facdiv  14355  hasheqf1oi  14419  hashnn0n0nn  14459  hashss  14477  hashgt12el  14491  hashgt12el2  14492  hashimarni  14510  hashle2pr  14546  pr2pwpr  14548  hashge2el2dif  14549  hashge2el2difr  14550  hashtpg  14554  hashge3el3dif  14556  exprelprel  14559  hash1to3  14561  hash3tpde  14562  tpfo  14569  fundmge2nop0  14571  fi1uzind  14576  ccatsymb  14652  swrdnd  14728  swrdnd2  14729  swrdnnn0nd  14730  swrdnd0  14731  pfxnd0  14762  swrdswrdlem  14777  swrdswrd  14778  pfxccatin12lem2a  14800  pfxccatin12lem1  14801  swrdccatin2  14802  pfxccatin12lem2  14804  pfxccatin12lem3  14805  pfxccat3  14807  swrdccat  14808  swrdccat3blem  14812  repsdf2  14853  repswswrd  14859  cshwidxmod  14878  cshwidx0  14881  cshf1  14885  cshweqrep  14896  cshw1  14897  2cshwcshw  14900  scshwfzeqfzo  14901  cshwcsh2id  14903  wwlktovfo  15035  relexpaddg  15130  iseraltlem2  15774  modfsummods  15884  clim2prod  15981  prodfn0  15987  prodfrec  15988  prodmo  16029  fprodabs  16067  binomfallfac  16133  fprodefsum  16187  dvdsaddre2b  16403  addmodlteqALT  16421  oddge22np1  16445  nn0enne  16473  nn0o1gt2  16477  sumeven  16483  sumodd  16484  dvdslegcd  16600  gcdneg  16618  dfgcd2  16642  rplpwr  16654  lcmf  16729  lcmftp  16732  lcmfunsnlem2lem1  16734  lcmfunsnlem2  16736  lcmfdvdsb  16739  coprmdvds1  16748  qredeq  16753  coprmprod  16757  coprmproddvdslem  16758  cncongr1  16763  cncongr2  16764  prm2orodd  16787  2mulprm  16789  nnnn0modprm0  16904  prm23lt5  16912  prm23ge5  16913  dvdsprmpweqnn  16983  dvdsprmpweqle  16984  oddprmdvds  17001  prmpwdvds  17002  prmreclem4  17017  ramcl  17127  prmgaplem6  17154  prmgaplem7  17155  prmgaplem8  17156  cshwshashlem1  17193  cshwshashlem2  17194  cshwshashlem3  17195  cshwrepswhash1  17200  setsn0fun  17271  setsstruct2  17272  imasleval  17633  mreiincl  17686  mreexexd  17742  inveq  17869  cicsym  17899  cictr  17900  initoid  18096  termoid  18097  initoeu2lem0  18108  initoeu2lem1  18109  initoeu2lem2  18110  initoeu2  18111  fthestrcsetc  18244  fthsetcestrc  18259  drsdirfi  18399  isnmgm  18740  mgmhmlin  18807  issubmgm2  18811  sgrpass  18833  insubm  18933  mgm2nsgrplem3  19038  dfgrp3lem  19167  cyccom  19337  symg2bas  19526  symgfix2  19549  symgextf1  19554  gsmsymgrfix  19561  pmtrprfv3  19587  psgnunilem4  19630  efgi2  19858  0ringnnzr  20692  rnghmsscmap  20798  rnghmsubcsetclem2  20800  rngcinv  20805  funcrngcsetc  20808  funcrngcsetcALT  20809  rhmsscmap  20827  rhmsubcsetclem2  20829  rhmsubcrngclem2  20835  ringcbasbas  20841  funcringcsetc  20842  rhmsubclem4  20856  unichnlidl  21431  rngqiprngimfo  21510  psgndiflemB  21819  psgndiflemA  21820  elfrlmbasn0  21982  lmictra  22064  mpfrcl  22307  gsummoncoe1  22539  mamufacex  22624  matecl  22653  dmatelnd  22724  dmatscmcl  22731  scmateALT  22740  scmatsgrp1  22750  scmatf1  22759  mavmulsolcl  22779  cramerimplem1  22914  cramerimplem2  22915  pmatcollpw3fi1  23019  mp2pm2mplem4  23040  pm2mpfo  23045  chmaidscmat  23079  fvmptnn04ifb  23082  chfacfscmul0  23089  chfacfpmmul0  23093  cayhamlem1  23097  cayhamlem3  23118  cayleyhamilton1  23123  fiinopn  23132  tgcl  23200  distop  23226  isclo2  23319  iscldtop  23326  ssnei2  23347  opnnei  23351  pnfnei  23451  mnfnei  23452  tgcnp  23484  cnpnei  23495  1stcelcls  23693  txcnpi  23840  cnmptcom  23910  fbfinnfr  24073  isfildlem  24089  snfil  24096  fbunfip  24101  fgcl  24110  elfm2  24180  fmco  24193  fbflim2  24209  cnpflf2  24232  flimfcls  24258  tmdgsum  24327  neibl  24733  tngngpim  24891  fgcfil  25505  caubl  25542  volsuplem  25789  ellimc3  26113  dvnadd  26163  dvnres  26165  cpnord  26169  dvnfre  26186  ply1divex  26369  plyconz  26547  cxpmul2  26934  fsumdvdsmul  27439  zabsle1  27540  gausslemma2dlem1a  27609  gausslemma2dlem3  27612  lgsquad2lem2  27629  2lgs  27651  2sq2  27677  2sqnn0  27682  2sqnn  27683  2sqreultlem  27691  2sqreunnltlem  27694  qabvexp  27870  ltsval2  27900  nolt02o  27939  sltsun1  28061  cutsun12  28063  madebday  28173  mulsprop  28403  precsexlem8  28487  precsexlem9  28488  noseqind  28565  om2noseqrdg  28577  n0cutlt  28632  peano5uzs  28677  expadds  28708  bdaypw2n0bndlem  28736  bdaypw2n0bnd  28737  axcontlem4  29432  umgredgprv  29572  umgrnloop  29573  upgrpredgv  29604  upgredgpr  29607  edglnl  29608  usgredgprvALT  29663  usgrnloopALT  29671  usgredg2v  29695  fusgrfis  29798  nbuhgr2vtx1edgblem  29819  nb3grprlem1  29848  cusgrsize2inds  29921  cusgrfi  29926  fusgrn0degnn0  29967  uspgrloopvtxel  29984  vtxdginducedm1lem4  30010  uhgr0edg0rgrb  30042  wlkl1loop  30105  wlk1walk  30106  upgriswlk  30108  upgrwlkvtxedg  30112  uspgr2wlkeq  30113  wlkv0  30117  wlksoneq1eq2  30130  wlkon2n0  30132  wlkreslem  30135  wlkres  30136  lfgrwlkprop  30157  pthdivtx  30199  2pthnloop  30204  spthonepeq  30225  uhgrwkspthlem2  30227  uhgrwkspth  30228  usgr2wlkneq  30229  usgr2trlncl  30233  usgr2pthlem  30236  usgr2pth  30237  cyclnspth  30276  spthcycl  30279  lfgrn1cycl  30281  usgr2trlncrct  30282  uspgrn2crct  30284  crctcshwlkn0lem3  30288  crctcshwlkn0lem5  30290  wwlknp  30319  wspthneq1eq2  30336  0enwwlksnge1  30340  wlklnwwlkln1  30344  wlkiswwlks2  30351  wlkiswwlksupgr2  30353  wlklnwwlkln2lem  30358  wwlksnred  30368  wwlksnextbi  30370  wwlksnredwwlkn0  30372  wwlksnextwrd  30373  wwlksnextinj  30375  wwlksnextproplem3  30387  wwlksnextprop  30388  wspthsnwspthsnon  30392  wspthsnonn0vne  30393  2pthon3v  30419  umgr2adedgwlkonALT  30423  umgr2wlk  30425  umgr2wlkon  30426  usgrwwlks2on  30434  umgrwwlks2on  30435  elwspths2on  30438  elwspths2onw  30439  usgr2wspthons3  30443  elwwlks2  30445  rusgrnumwwlk  30454  clwwlkccatlem  30467  clwlkclwwlklem2a4  30475  clwlkclwwlklem2a  30476  clwlkclwwlklem2  30478  clwlkclwwlkf1lem3  30484  erclwwlkeqlen  30497  clwwlknwwlksn  30516  loopclwwlkn1b  30520  clwwlkf1  30527  wwlksext2clwwlk  30535  eleclclwwlknlem2  30539  umgr2cwwk2dif  30542  eleclclwwlkn  30554  hashecclwwlkn1  30555  umgrhashecclwwlk  30556  clwwlknonwwlknonb  30584  clwwlknonex2lem2  30586  clwwlknonex2  30587  loop1cycl  30631  1pthon2v  30641  upgr3v3e3cycl  30668  uhgr3cyclexlem  30669  uhgr3cyclex  30670  eupth2lem3lem4  30719  frgr3vlem1  30761  frgr3vlem2  30762  3vfriswmgrlem  30765  3vfriswmgr  30766  3cyclfrgrrn1  30773  n4cyclfrgr  30779  frgrncvvdeqlem3  30789  frgrncvvdeqlem6  30792  frgrncvvdeqlem7  30793  frgrncvvdeqlem8  30794  frgrwopreglem4a  30798  frgrwopreglem3  30802  frgrwopreg1  30806  frgrwopreg2  30807  frgrwopreglem5lem  30808  frgrwopreglem5ALT  30810  frgrwopreg  30811  fusgr2wsp2nb  30822  2wspmdisj  30825  numclwwlk1lem2foa  30842  numclwwlk1lem2f1  30845  numclwwlk1lem2fo  30846  numclwwlk1  30849  wlkl0  30855  numclwwlk2lem1  30864  numclwlk2lem2f  30865  numclwlk2lem2f1o  30867  frgrreg  30882  frgrregord013  30883  frgrregord13  30884  friendshipgt3  30886  friendship  30887  eulplig  30974  ipassi  31330  ubthlem2  31360  isch3  31730  shintcli  31818  shmodsi  31878  spansncvi  32141  hoaddsub  32305  eigorthi  32326  pjss2coi  32653  pjnormssi  32657  pj3cor1i  32698  strb  32747  dmdmd  32789  mdsl0  32799  csmdsymi  32823  chrelat2i  32854  mdsymlem3  32894  mdsymlem6  32897  sumdmdlem2  32908  opreu2reuALT  32960  ssrelf  33096  gsumwun  33524  r1filim  35620  trssfir1om  35629  fineqvinfep  35659  trssfir1omregs  35670  karddom  35695  kardsdom  35696  kardexen  35697  onvf1odlem4  35711  cvmlift2lem1  35889  satfrel  35954  satfrnmapom  35957  fmlafvel  35972  fmla1  35974  gonarlem  35981  gonar  35982  goalrlem  35983  goalr  35984  satffunlem  35988  satffunlem1lem1  35989  satffunlem2lem1  35991  satffun  35996  satefvfmla1  36012  mrsubvrs  36109  mclsax  36156  3ccased  36306  dfon2lem3  36370  rdgprc  36379  cgrextend  36596  btwndiff  36615  btwnconn1lem12  36686  brsegle  36696  broutsideof2  36710  funray  36728  in-ax8  36852  ss-ax8  36853  elicc3  36944  nn0prpwlem  36949  nn0prpw  36950  fnessref  36984  neibastop2lem  36987  filnetlem4  37008  meran1  37038  waj-ax  37041  arg-ax  37043  axtco1from2  37102  dfttc4  37157  mh-inf3f1  37168  mh-regprimbi  37172  bj-nnclavc  37252  bj-con2com  37269  bj-axdd2  37301  bj-alrimg  37322  bj-exlimg  37344  bj-exalimi  37354  bj-eximcom  37355  bj-ssbid1ALT  37403  bj-sb  37428  bj-snsetex  37715  bj-axseprep  37827  bj-axreprepsep  37828  bj-restpw  37850  bj-finsumval0  38045  mptsnunlem  38100  icoreclin  38119  relowlpssretop  38126  inunissunidif  38137  rdgssun  38140  finorwe  38144  domalom  38166  wl-dral1d  38302  wl-exeq  38305  wl-lem-exsb  38337  wl-eujustlem1  38359  poimirlem29  38406  poimirlem32  38409  findcard4  38471  fdc  38503  seqpo  38505  incsequz  38506  isismty  38559  ismtybndlem  38564  heibor1lem  38567  ismgmOLD  38608  isexid2  38613  ghomco  38649  pridlc  38829  relcnveq3  39083  elrelscnveq3  39383  cdleme18d  41176  tendovalco  41646  cdlemn11pre  42091  dihord2pre  42106  indstrd  43067  unitscyglem3  43071  eu6w  43530  incssnn0  43564  fphpd  43665  jm2.19lem3  43840  setindtr  43873  islssfg2  43920  mpaaeu  43999  ordnexbtwnsuc  44116  oaabsb  44143  succlg  44177  oacl2g  44179  omabs2  44181  omcl2  44182  omcl3g  44183  pr2cv  44396  refimssco  44455  iunrelexpmin1  44556  iunrelexpmin2  44560  trclimalb2  44574  clsk1indlem3  44891  tfindsd  45056  mnurndlem1  45113  nzss  45149  sb5ALT  45356  truniALT  45372  ee223  45465  3orbi123VD  45680  sbc3orgVD  45681  exbirVD  45683  exbiriVD  45684  sbcim2gVD  45705  trsbcVD  45707  truniALTVD  45708  onfrALTlem3VD  45717  onfrALTlem2VD  45719  csbrngVD  45726  19.41rgVD  45732  ax6e2eqVD  45737  ax6e2ndeqVD  45739  2uasbanhVD  45741  sb5ALTVD  45743  vk15.4jVD  45744  infxrunb3rnmpt  46264  stoweidlem26  46862  et-equeucl  47708  hirstL-ax3  47788  rexsb  47995  rexrsb  47996  euoreqb  48005  2reu8i  48009  afvres  48068  tz6.12-afv  48069  afvco2  48072  afv2orxorb  48124  afv2res  48135  tz6.12-afv2  48136  tz6.12i-afv2  48139  dfatcolem  48151  zm1nn  48198  2ffzoeq  48224  smonoord  48273  iccpartiltu  48330  iccpartlt  48332  iccpartltu  48333  iccpartgtl  48334  iccpartgt  48335  iccpartleu  48336  iccpartgel  48337  icceuelpart  48344  iccpartnel  48346  lswn0  48352  ichnreuop  48380  ichreuopeq  48381  prsprel  48395  sprsymrelfvlem  48398  sprsymrelf1lem  48399  sprsymrelfolem2  48401  prproropf1olem4  48414  paireqne  48419  prprelb  48424  reupr  48430  goldbachth  48458  odz2prm2pw  48474  fmtno4prmfac  48483  fmtno4prmfac193  48484  prmdvdsfmtnof1lem2  48496  2pwp1prmfmtno  48501  lighneallem2  48517  lighneallem4b  48520  lighneallem4  48521  requad2  48547  odd2prm2  48642  mogoldbblem  48644  gbepos  48682  gbowgt5  48686  gbowge7  48687  stgoldbwt  48700  sbgoldbwt  48701  sbgoldbst  48702  sbgoldbaltlem1  48703  sbgoldbalt  48705  sbgoldbo  48711  nnsum3primesle9  48718  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  bgoldbtbndlem1  48729  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  bgoldbtbnd  48733  dfnbgr6  48781  isuspgrimlem  48819  uhgrimisgrgric  48855  clnbgrgrim  48858  usgrgrtrirex  48874  isubgr3stgrlem4  48893  grilcbri2  48935  grlicsym  48937  grlictr  48939  gricgrlic  48942  gpgvtxedg0  48987  gpgvtxedg1  48988  gpgedg2ov  48990  gpgedg2iv  48991  pgnioedg1  49032  pgnioedg2  49033  pgnioedg3  49034  pgnioedg4  49035  pgnioedg5  49036  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem3  49042  pgnbgreunbgrlem5lem1  49044  pgnbgreunbgrlem5lem2  49045  pgnbgreunbgrlem5lem3  49046  pgnbgreunbgrlem6  49048  upgrwlkupwlk  49064  uspgrsprf1  49071  lmod0rng  49152  lidldomn1  49154  rngccatidALTV  49195  rngcinvALTV  49199  rhmsubcALTVlem4  49207  funcringcsetcALTV2lem9  49221  ringccatidALTV  49229  ringcbasbasALTV  49235  ztprmneprm  49285  pgrpgt2nabl  49304  lmodvsmdi  49317  ply1mulgsumlem2  49325  lincsumcl  49369  ellcoellss  49373  linindslinci  49386  islinindfis  49387  lincext3  49394  lindslinindimp2lem4  49399  lindslinindsimp2lem5  49400  lindslinindsimp2  49401  lindsrng01  49406  ldepspr  49411  lincresunit3lem1  49417  elfzolborelfzop1  49457  dignn0ldlem  49540  nn0sumshdiglem1  49559  1arymaptf1  49580  2arymaptf1  49591  rrx2xpref1o  49656  rrx2plord2  49660  rrx2plordisom  49661  line2ylem  49689  line2xlem  49691  line2y  49693  itschlc0xyqsol1  49704  inlinecirc02plem  49724  fullthinc  50384  tfis2d  50614  onsetrec  50642