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  2216  sbiedw  2347  cbv1v  2366  exsb  2389  cbv1  2432  ax12b  2454  axc11n  2456  dvelimdf  2479  equvel  2486  dfsb1  2511  sbied  2533  dfmoeu  2561  mo3  2590  mo4  2592  2mo  2674  2eu6  2682  exists2  2687  pm2.61dne  3042  rexlimdv  3162  r19.21v  3188  r19.12  3312  2gencl  3493  3gencl  3494  vtocl2ga  3538  vtocl2gaf  3539  vtocl3gaf  3540  vtocl3ga  3541  vtocl4ga  3543  rspccv  3574  ceqex  3606  mob  3675  euind  3682  reuind  3711  2reu1  3845  sseq2  3957  nelss  3997  rexdifi  4097  reupick2  4277  disjeq0  4409  uneqdifeq  4448  sspw  4568  ssprsseq  4786  preq12b  4810  prnebg  4816  prel12g  4824  3elpr2eq  4866  iinss2  5016  trintss  5231  dtruALT2  5332  reusv2lem1  5360  alxfr  5369  ralxfrALT  5377  exexneq  5403  copsexgwOLD  5461  snopeqop  5478  propeqop  5479  opthhausdorff  5490  opthhausdorff0  5491  pofun  5577  solin  5586  frss  5615  2optocl  5747  3optocl  5748  ssrel  5759  ssrel2  5761  ssrelrel  5772  elrelb  5775  relop  5828  dfres3  5975  asymref2  6109  xpidtr  6114  trin2  6115  poltletr  6124  xp11  6166  imadifssranOLD  6196  relcnvtrgOLD  6262  reuop  6289  tz7.7  6381  ordtr2  6401  suc11  6465  fundif  6581  fss  6718  f0dom0  6758  fv3  6895  tz6.12i  6903  mpteqb  7005  fveqdmss  7070  eldmrexrnb  7084  funopsnOLD  7144  funsndifnop  7147  tpres  7199  funfvima  7228  fvclss  7237  f1veqaeq  7252  fvf1pr  7307  isoselem  7341  oprabv  7472  ovg  7577  elovmpt3rab1  7673  sorpsscmpl  7739  iunpw  7774  trom  7875  limom  7882  peano5  7894  focdmex  7957  funelss  8047  funeldmdif  8048  bropopvvv  8090  bropfvvvvlem  8091  f1o2ndf1  8122  poxp  8129  soxp  8130  poxp2  8144  frxp2  8145  frxp3  8152  suppimacnv  8175  ressuppss  8184  ressuppssdif  8186  tposfn2  8249  wfr3g  8321  onnseq  8336  smoel  8352  smogt  8359  smoiso2  8361  tfr3  8391  tz7.48-2  8436  tz7.48-3  8438  tz7.49  8439  oecl  8529  oaordex  8550  oalimcl  8552  oaass  8553  omordi  8558  omlimcl  8570  odi  8571  omeulem1  8574  oen0  8579  nnawordi  8614  nnaass  8615  nnmordi  8624  omabs  8644  omsmolem  8650  naddssim  8679  brinxper  8731  iiner  8794  2ecoptocl  8813  3ecoptocl  8814  undifixp  8946  xpdom2  9075  xpf1o  9142  infensuc  9158  findcard2  9164  php  9206  isinf  9240  unblem2  9269  fodomfir  9303  infssuni  9319  finsschain  9332  fsuppunfi  9364  fsuppunbi  9365  marypha1  9410  hartogs  9522  card2on  9532  card2inf  9533  xpwdomg  9563  elirrvOLD  9576  elirrvOLDOLD  9577  en3lp  9599  preleqg  9600  inf3lem1  9613  inf3lem2  9614  inf3lem3  9615  inf3lem5  9617  noinfep  9645  ttrclss  9705  ttrclselem2  9711  trcl  9713  tcel  9728  frr3g  9744  rankonidlem  9819  elhf4  9893  scottexOLD  9915  djuunxp  9983  eldju2ndl  9986  updjud  9996  dif1card  10070  fodomnum  10117  cardaleph  10149  kmlem9  10218  kmlem13  10222  cflim2  10322  cfsmolem  10329  infpssrlem3  10364  isfin7-2  10455  fin1a2lem6  10464  fin1a2lem12  10470  domtriomlem  10501  axdc3lem4  10512  axdc4lem  10514  zorn2lem3  10557  zorn2lem4  10558  zorn2lem5  10559  zorn2lem7  10561  zornn0g  10564  axdclem2  10579  ondomon  10628  alephval2  10638  cfpwsdom  10650  wuncval2  10813  grupr  10863  gruiun  10865  ingru  10881  grothomex  10895  indpi  10973  nqereu  10995  prlem934  11099  reclem2pr  11114  mulgt0sr  11171  supsrlem  11177  1re  11289  dedekind  11454  lemul1a  12152  squeeze0  12201  peano5nni  12319  nnadddir  12375  nnunb  12583  nn0lt2  12743  nn0le2is012  12744  fzind  12778  nn0ind-raph  12780  zindd  12781  uzin  12982  nn01to3  13049  xnn0xadd0  13358  xmulasslem  13396  icoshft  13585  fzen  13654  uzsubsubfz  13660  elfz0ubfz0  13746  elfz0fzfz0  13747  fz0fzelfz0  13748  elfzmlbp  13753  elfzodifsumelfzo  13846  ssfzo12bi  13876  fzoopth  13877  elfzonelfzo  13884  elfznelfzo  13888  injresinjlem  13905  injresinj  13906  modfzo0difsn  14066  modsumfzodifsn  14067  addmodlteq  14069  ssnn0fi  14108  fsuppmapnn0fiub0  14116  expcllem  14195  expeq0  14215  mulexp  14224  leexp2r  14297  bernneq  14353  facdiv  14411  hasheqf1oi  14475  hashnn0n0nn  14515  hashss  14533  hashgt12el  14547  hashgt12el2  14548  hashimarni  14566  hashle2pr  14602  pr2pwpr  14604  hashge2el2dif  14605  hashge2el2difr  14606  hashtpg  14610  hashge3el3dif  14612  exprelprel  14615  hash1to3  14617  hash3tpde  14618  tpfo  14625  fundmge2nop0  14627  fi1uzind  14632  ccatsymb  14708  swrdnd  14784  swrdnd2  14785  swrdnnn0nd  14786  swrdnd0  14787  pfxnd0  14818  swrdswrdlem  14833  swrdswrd  14834  pfxccatin12lem2a  14856  pfxccatin12lem1  14857  swrdccatin2  14858  pfxccatin12lem2  14860  pfxccatin12lem3  14861  pfxccat3  14863  swrdccat  14864  swrdccat3blem  14868  repsdf2  14909  repswswrd  14915  cshwidxmod  14934  cshwidx0  14937  cshf1  14941  cshweqrep  14952  cshw1  14953  2cshwcshw  14956  scshwfzeqfzo  14957  cshwcsh2id  14959  wwlktovfo  15091  relexpaddg  15186  iseraltlem2  15830  modfsummods  15940  clim2prod  16037  prodfn0  16043  prodfrec  16044  prodmo  16083  fprodabs  16121  binomfallfac  16187  fprodefsum  16241  dvdsaddre2b  16457  addmodlteqALT  16475  oddge22np1  16499  nn0enne  16527  nn0o1gt2  16531  sumeven  16537  sumodd  16538  dvdslegcd  16654  gcdneg  16674  dfgcd2  16699  rplpwr  16712  lcmf  16788  lcmftp  16791  lcmfunsnlem2lem1  16793  lcmfunsnlem2  16795  lcmfdvdsb  16798  coprmdvds1  16807  qredeq  16812  coprmprod  16816  coprmproddvdslem  16817  cncongr1  16822  cncongr2  16823  prm2orodd  16846  2mulprm  16848  nnnn0modprm0  16964  prm23lt5  16972  prm23ge5  16973  dvdsprmpweqnn  17043  dvdsprmpweqle  17044  oddprmdvds  17061  prmpwdvds  17062  prmreclem4  17077  ramcl  17187  prmgaplem6  17214  prmgaplem7  17215  prmgaplem8  17216  cshwshashlem1  17253  cshwshashlem2  17254  cshwshashlem3  17255  cshwrepswhash1  17260  setsn0fun  17331  setsstruct2  17332  imasleval  17693  mreiincl  17746  mreexexd  17802  inveq  17929  cicsym  17959  cictr  17960  initoid  18156  termoid  18157  initoeu2lem0  18168  initoeu2lem1  18169  initoeu2lem2  18170  initoeu2  18171  fthestrcsetc  18304  fthsetcestrc  18319  drsdirfi  18459  isnmgm  18800  mgmhmlin  18868  issubmgm2  18872  sgrpass  18894  insubm  18994  mgm2nsgrplem3  19099  dfgrp3lem  19228  cyccom  19398  symg2bas  19587  symgfix2  19610  symgextf1  19615  gsmsymgrfix  19622  pmtrprfv3  19648  psgnunilem4  19691  efgi2  19919  0ringnnzr  20756  rnghmsscmap  20862  rnghmsubcsetclem2  20864  rngcinv  20869  funcrngcsetc  20872  funcrngcsetcALT  20873  rhmsscmap  20891  rhmsubcsetclem2  20893  rhmsubcrngclem2  20899  ringcbasbas  20905  funcringcsetc  20906  rhmsubclem4  20920  unichnlidl  21496  rngqiprngimfo  21577  psgndiflemB  21886  psgndiflemA  21887  elfrlmbasn0  22049  lmictra  22131  mpfrcl  22374  gsummoncoe1  22606  mamufacex  22691  matecl  22720  dmatelnd  22791  dmatscmcl  22798  scmateALT  22807  scmatsgrp1  22817  scmatf1  22826  mavmulsolcl  22846  cramerimplem1  22981  cramerimplem2  22982  pmatcollpw3fi1  23086  mp2pm2mplem4  23107  pm2mpfo  23112  chmaidscmat  23146  fvmptnn04ifb  23149  chfacfscmul0  23156  chfacfpmmul0  23160  cayhamlem1  23164  cayhamlem3  23185  cayleyhamilton1  23190  fiinopn  23199  tgcl  23267  distop  23293  isclo2  23386  iscldtop  23393  ssnei2  23414  opnnei  23418  pnfnei  23518  mnfnei  23519  tgcnp  23551  cnpnei  23562  1stcelcls  23760  txcnpi  23907  cnmptcom  23977  fbfinnfr  24140  isfildlem  24156  snfil  24163  fbunfip  24168  fgcl  24177  elfm2  24247  fmco  24260  fbflim2  24276  cnpflf2  24299  flimfcls  24325  tmdgsum  24394  neibl  24800  tngngpim  24958  fgcfil  25572  caubl  25609  volsuplem  25856  ellimc3  26179  dvnadd  26229  dvnres  26231  cpnord  26235  dvnfre  26252  ply1divex  26435  plyconz  26613  cxpmul2  26999  fsumdvdsmul  27504  zabsle1  27605  gausslemma2dlem1a  27674  gausslemma2dlem3  27677  lgsquad2lem2  27694  2lgs  27716  2sq2  27742  2sqnn0  27747  2sqnn  27748  2sqreultlem  27756  2sqreunnltlem  27759  qabvexp  27935  ltsval2  27995  nolt02o  28034  sltsun1  28156  cutsun12  28158  madebday  28268  mulsprop  28498  precsexlem8  28582  precsexlem9  28583  noseqind  28660  om2noseqrdg  28672  n0cutlt  28727  peano5uzs  28772  expadds  28803  bdaypw2n0bndlem  28831  bdaypw2n0bnd  28832  axcontlem4  29527  umgredgprv  29667  umgrnloop  29668  upgrpredgv  29699  upgredgpr  29702  edglnl  29703  usgredgprvALT  29758  usgrnloopALT  29766  usgredg2v  29790  fusgrfis  29893  nbuhgr2vtx1edgblem  29914  nb3grprlem1  29943  cusgrsize2inds  30016  cusgrfi  30021  fusgrn0degnn0  30062  uspgrloopvtxel  30079  vtxdginducedm1lem4  30105  uhgr0edg0rgrb  30137  wlkl1loop  30200  wlk1walk  30201  upgriswlk  30203  upgrwlkvtxedg  30207  uspgr2wlkeq  30208  wlkv0  30212  wlksoneq1eq2  30225  wlkon2n0  30227  wlkreslem  30230  wlkres  30231  lfgrwlkprop  30252  pthdivtx  30294  2pthnloop  30299  spthonepeq  30320  uhgrwkspthlem2  30322  uhgrwkspth  30323  usgr2wlkneq  30324  usgr2trlncl  30328  usgr2pthlem  30331  usgr2pth  30332  cyclnspth  30371  spthcycl  30374  lfgrn1cycl  30376  usgr2trlncrct  30377  uspgrn2crct  30379  crctcshwlkn0lem3  30383  crctcshwlkn0lem5  30385  wwlknp  30414  wspthneq1eq2  30431  0enwwlksnge1  30435  wlklnwwlkln1  30439  wlkiswwlks2  30446  wlkiswwlksupgr2  30448  wlklnwwlkln2lem  30453  wwlksnred  30463  wwlksnextbi  30465  wwlksnredwwlkn0  30467  wwlksnextwrd  30468  wwlksnextinj  30470  wwlksnextproplem3  30482  wwlksnextprop  30483  wspthsnwspthsnon  30487  wspthsnonn0vne  30488  2pthon3v  30514  umgr2adedgwlkonALT  30518  umgr2wlk  30520  umgr2wlkon  30521  usgrwwlks2on  30529  umgrwwlks2on  30530  elwspths2on  30533  elwspths2onw  30534  usgr2wspthons3  30538  elwwlks2  30540  rusgrnumwwlk  30549  clwwlkccatlem  30562  clwlkclwwlklem2a4  30570  clwlkclwwlklem2a  30571  clwlkclwwlklem2  30573  clwlkclwwlkf1lem3  30579  erclwwlkeqlen  30592  clwwlknwwlksn  30611  loopclwwlkn1b  30615  clwwlkf1  30622  wwlksext2clwwlk  30630  eleclclwwlknlem2  30634  umgr2cwwk2dif  30637  eleclclwwlkn  30649  hashecclwwlkn1  30650  umgrhashecclwwlk  30651  clwwlknonwwlknonb  30679  clwwlknonex2lem2  30681  clwwlknonex2  30682  loop1cycl  30726  1pthon2v  30736  upgr3v3e3cycl  30763  uhgr3cyclexlem  30764  uhgr3cyclex  30765  eupth2lem3lem4  30814  frgr3vlem1  30856  frgr3vlem2  30857  3vfriswmgrlem  30860  3vfriswmgr  30861  3cyclfrgrrn1  30868  n4cyclfrgr  30874  frgrncvvdeqlem3  30884  frgrncvvdeqlem6  30887  frgrncvvdeqlem7  30888  frgrncvvdeqlem8  30889  frgrwopreglem4a  30893  frgrwopreglem3  30897  frgrwopreg1  30901  frgrwopreg2  30902  frgrwopreglem5lem  30903  frgrwopreglem5ALT  30905  frgrwopreg  30906  fusgr2wsp2nb  30917  2wspmdisj  30920  numclwwlk1lem2foa  30937  numclwwlk1lem2f1  30940  numclwwlk1lem2fo  30941  numclwwlk1  30944  wlkl0  30950  numclwwlk2lem1  30959  numclwlk2lem2f  30960  numclwlk2lem2f1o  30962  frgrreg  30977  frgrregord013  30978  frgrregord13  30979  friendshipgt3  30981  friendship  30982  eulplig  31069  ipassi  31425  ubthlem2  31455  isch3  31825  shintcli  31913  shmodsi  31973  spansncvi  32236  hoaddsub  32400  eigorthi  32421  pjss2coi  32748  pjnormssi  32752  pj3cor1i  32793  strb  32842  dmdmd  32884  mdsl0  32894  csmdsymi  32918  chrelat2i  32949  mdsymlem3  32989  mdsymlem6  32992  sumdmdlem2  33003  opreu2reuALT  33055  ssrelf  33191  gsumwun  33619  r1filim  35708  trssfir1om  35716  fineqvinfep  35766  trssfir1omregs  35777  karddom  35802  kardsdom  35803  kardexen  35804  onvf1odlem4  35858  cvmlift2lem1  36036  satfrel  36101  satfrnmapom  36104  fmlafvel  36119  fmla1  36121  gonarlem  36128  gonar  36129  goalrlem  36130  goalr  36131  satffunlem  36135  satffunlem1lem1  36136  satffunlem2lem1  36138  satffun  36143  satefvfmla1  36159  mrsubvrs  36256  mclsax  36303  3ccased  36453  dfon2lem3  36517  rdgprc  36526  cgrextend  36743  btwndiff  36762  btwnconn1lem12  36833  brsegle  36843  broutsideof2  36857  funray  36875  in-ax8  36983  ss-ax8  36984  elicc3  37075  nn0prpwlem  37080  nn0prpw  37081  fnessref  37115  neibastop2lem  37118  filnetlem4  37139  meran1  37169  waj-ax  37172  arg-ax  37174  axtco1from2  37233  dfttc4  37288  mh-inf3f1  37299  mh-regprimbi  37303  bj-nnclavc  37383  bj-con2com  37400  bj-axdd2  37432  bj-alrimg  37453  bj-exlimg  37475  bj-exalimi  37485  bj-eximcom  37486  bj-ssbid1ALT  37534  bj-sb  37559  bj-snsetex  37846  bj-axseprep  37958  bj-axreprepsep  37959  bj-restpw  37981  bj-finsumval0  38174  mptsnunlem  38229  icoreclin  38248  relowlpssretop  38255  inunissunidif  38266  rdgssun  38269  finorwe  38273  domalom  38295  wl-dral1d  38431  wl-exeq  38434  wl-lem-exsb  38466  wl-eujustlem1  38488  poimirlem29  38535  poimirlem32  38538  findcard4  38600  fdc  38647  seqpo  38649  incsequz  38650  isismty  38703  ismtybndlem  38708  heibor1lem  38711  ismgmOLD  38752  isexid2  38757  ghomco  38793  pridlc  38973  relcnveq3  39227  elrelscnveq3  39527  cdleme18d  41320  tendovalco  41790  cdlemn11pre  42235  dihord2pre  42250  indstrd  43211  unitscyglem3  43215  eu6w  43641  incssnn0  43675  fphpd  43776  jm2.19lem3  43951  setindtr  43984  islssfg2  44031  mpaaeu  44110  ordnexbtwnsuc  44227  oaabsb  44254  succlg  44288  oacl2g  44290  omabs2  44292  omcl2  44293  omcl3g  44294  pr2cv  44507  refimssco  44566  iunrelexpmin1  44667  iunrelexpmin2  44671  trclimalb2  44685  clsk1indlem3  45002  tfindsd  45167  mnurndlem1  45224  nzss  45260  sb5ALT  45467  truniALT  45483  ee223  45576  3orbi123VD  45791  sbc3orgVD  45792  exbirVD  45794  exbiriVD  45795  sbcim2gVD  45816  trsbcVD  45818  truniALTVD  45819  onfrALTlem3VD  45828  onfrALTlem2VD  45830  csbrngVD  45837  19.41rgVD  45843  ax6e2eqVD  45848  ax6e2ndeqVD  45850  2uasbanhVD  45852  sb5ALTVD  45854  vk15.4jVD  45855  infxrunb3rnmpt  46382  stoweidlem26  46980  et-equeucl  47826  hirstL-ax3  47906  rexsb  48113  rexrsb  48114  euoreqb  48123  2reu8i  48127  afvres  48186  tz6.12-afv  48187  afvco2  48190  afv2orxorb  48242  afv2res  48253  tz6.12-afv2  48254  tz6.12i-afv2  48257  dfatcolem  48269  zm1nn  48316  2ffzoeq  48342  smonoord  48391  iccpartiltu  48448  iccpartlt  48450  iccpartltu  48451  iccpartgtl  48452  iccpartgt  48453  iccpartleu  48454  iccpartgel  48455  icceuelpart  48462  iccpartnel  48464  lswn0  48470  ichnreuop  48498  ichreuopeq  48499  prsprel  48513  sprsymrelfvlem  48516  sprsymrelf1lem  48517  sprsymrelfolem2  48519  prproropf1olem4  48532  paireqne  48537  prprelb  48542  reupr  48548  goldbachth  48576  odz2prm2pw  48592  fmtno4prmfac  48601  fmtno4prmfac193  48602  prmdvdsfmtnof1lem2  48614  2pwp1prmfmtno  48619  lighneallem2  48635  lighneallem4b  48638  lighneallem4  48639  requad2  48665  odd2prm2  48760  mogoldbblem  48762  gbepos  48800  gbowgt5  48804  gbowge7  48805  stgoldbwt  48818  sbgoldbwt  48819  sbgoldbst  48820  sbgoldbaltlem1  48821  sbgoldbalt  48823  sbgoldbo  48829  nnsum3primesle9  48836  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  bgoldbtbndlem1  48847  bgoldbtbndlem2  48848  bgoldbtbndlem3  48849  bgoldbtbnd  48851  dfnbgr6  48899  isuspgrimlem  48937  uhgrimisgrgric  48973  clnbgrgrim  48976  usgrgrtrirex  48992  isubgr3stgrlem4  49011  grilcbri2  49053  grlicsym  49055  grlictr  49057  gricgrlic  49060  gpgvtxedg0  49105  gpgvtxedg1  49106  gpgedg2ov  49108  gpgedg2iv  49109  pgnioedg1  49150  pgnioedg2  49151  pgnioedg3  49152  pgnioedg4  49153  pgnioedg5  49154  pgnbgreunbgrlem2lem3  49158  pgnbgreunbgrlem3  49160  pgnbgreunbgrlem5lem1  49162  pgnbgreunbgrlem5lem2  49163  pgnbgreunbgrlem5lem3  49164  pgnbgreunbgrlem6  49166  upgrwlkupwlk  49182  uspgrsprf1  49189  lmod0rng  49270  lidldomn1  49272  rngccatidALTV  49313  rngcinvALTV  49317  rhmsubcALTVlem4  49325  funcringcsetcALTV2lem9  49339  ringccatidALTV  49347  ringcbasbasALTV  49353  ztprmneprm  49403  pgrpgt2nabl  49422  lmodvsmdi  49435  ply1mulgsumlem2  49443  lincsumcl  49487  ellcoellss  49491  linindslinci  49504  islinindfis  49505  lincext3  49512  lindslinindimp2lem4  49517  lindslinindsimp2lem5  49518  lindslinindsimp2  49519  lindsrng01  49524  ldepspr  49529  lincresunit3lem1  49535  elfzolborelfzop1  49575  dignn0ldlem  49658  nn0sumshdiglem1  49677  1arymaptf1  49698  2arymaptf1  49709  rrx2xpref1o  49774  rrx2plord2  49778  rrx2plordisom  49779  line2ylem  49807  line2xlem  49809  line2y  49811  itschlc0xyqsol1  49822  inlinecirc02plem  49842  fullthinc  50502  tfis2d  50731  onsetrec  50745