Theorem pm2.61i 184

Description: Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2023.)

Hypotheses

Ref	Expression
pm2.61i.1	⊢ (𝜑 → 𝜓)
pm2.61i.2	⊢ (¬ 𝜑 → 𝜓)

Assertion

Ref	Expression
pm2.61i	⊢ 𝜓

Proof of Theorem pm2.61i

Step	Hyp	Ref	Expression
1		pm2.61i.1	. . 3 ⊢ (𝜑 → 𝜓)
2		pm2.61i.2	. . 3 ⊢ (¬ 𝜑 → 𝜓)
3	1, 2	nsyl4 159	. 2 ⊢ (¬ 𝜓 → 𝜓)
4	3	pm2.18i 130	1 ⊢ 𝜓

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

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

This theorem is used by:  pm2.61ii  185  pm2.61nii  186  pm2.61iii  187  pm2.65iOLD  197  pm5.21nii  381  pm5.18  384  biass  388  pm2.61ian  823  ecase3  1048  4cases  1056  pm4.42  1069  ifpid  1093  elimh  1099  3ecase  1505  norass  1567  ax6e  2415  ax12  2455  exdistrf  2479  equvini  2487  ax12vALT  2501  2ax6e  2503  sb1  2510  sb2  2511  sb4a  2512  dfsb1  2513  dfsb2  2525  sbcom3  2538  sbco2  2543  sbco3  2545  sb9  2551  eujustALT  2600  pm2.61ine  3041  ralcom2  3366  eueq2  3673  moeq3  3675  mo2icl  3677  sbc2or  3753  unineq  4241  csb0  4375  sbcel12  4376  sbcne12  4380  sbcel2  4383  csbidm  4398  csbun  4406  csbin  4407  csbdif  4486  ifsb  4501  ifid  4528  ifnot  4540  ifan  4541  ifor  4542  csbif  4545  elimhyp  4553  elimhyp2v  4554  elimhyp3v  4555  elimhyp4v  4556  elimdhyp  4558  keephyp2v  4560  keephyp3v  4561  rmosn  4685  rabsnif  4689  tppreqb  4773  ssunsn2  4793  n0snor2el  4798  preq12nebg  4828  opthprneg  4830  elpreqprlem  4831  dfopif  4835  csbuni  4903  disjord  5098  sbcbr  5166  unisn2  5275  intabs  5319  class2set  5325  dtruALT2  5341  snexALT  5354  dtruALT  5359  axprlem3  5396  axprlem3OLD  5400  axprglem  5407  axprg  5408  snexOLD  5413  exneq  5417  copsexgwOLD  5473  copsexg  5474  snopeqop  5489  csbopab  5540  dfid3  5559  csbxp  5762  csbcnv  5872  csbres  5981  csbima12  6081  soirri  6126  csbrn  6204  dmsnopss  6215  dmsnsnsn  6221  opswap  6230  unixpid  6285  predres  6340  nsuceq0  6446  ordsssuc2  6454  iotassuni  6511  iotaex  6512  csbiota  6529  dffv3  6877  fvrn0  6909  ndmfv  6913  elfv2ex  6924  fveqres  6925  csbfv12  6926  csbfv  6928  dffv2  6976  fvco4i  6983  fvmptss  7002  fvmptex  7004  fvmptss2  7016  fvmptrabfv  7022  f0cli  7093  fvunsn  7177  fconst5  7204  csbriota  7382  riotassuni  7407  oprabidw  7441  csbov123  7454  csbov  7455  fvmptopab  7465  brfvopab  7467  elimdelov  7506  ovif12  7510  ifmpt2v  7512  ndmovcl  7595  ndmovord  7600  elovmpt3imp  7667  difsnexi  7756  ordsuc  7806  ordsucelsuc  7814  1stval  7984  2ndval  7985  1st2val  8010  2nd2val  8011  el2mpocsbcl  8076  bropopvvv  8081  bropfvvvvlem  8082  bropfvvvv  8083  suppimacnv  8166  suppssdm  8169  ressuppss  8175  suppun  8176  extmptsuppeq  8180  funsssuppss  8182  fczsupp0  8185  suppss  8186  suppss2  8192  suppssfv  8194  suppco  8198  mpoxopynvov0  8210  mpoxopoveqd  8213  pwuninelOLD  8268  smofvon2  8339  om0x  8500  mapssfset  8844  brdomg  8951  snfi  9036  sdomirr  9098  domunsn  9111  2pwuninel  9116  unfi  9151  cnvfi  9156  suppeqfsuppbi  9335  fsuppun  9343  funsnfsupp  9348  fipwuni  9382  oicl  9487  oif  9488  wemapso2  9511  card2on  9512  en2lp  9571  ttrclselem1  9690  tctr  9703  r1tr  9744  rankdmr1  9769  r1pw  9813  r1pwALT  9814  rankuni  9831  scottex  9858  scottexOLD  9859  cardidm  9950  alephcard  10059  alephnbtwn  10060  cfub  10236  cardcf  10239  cflecard  10240  cfle  10241  cflim2  10251  cfidm  10263  isf32lem9  10349  itunisuc  10407  itunitc1  10408  itunitc  10409  ituniiun  10410  axcc2lem  10424  alephreg  10571  pwcfsdom  10572  cfpwsdom  10573  axunndlem1  10584  axpownd  10590  tskmcl  10830  addcompi  10883  addasspi  10884  mulcompi  10885  mulasspi  10886  distrpi  10887  addnidpi  10890  nlt1pi  10895  addcompq  10939  addcomnq  10940  mulcompq  10941  mulcomnq  10942  adderpq  10945  mulerpq  10946  addassnq  10947  mulassnq  10948  distrnq  10950  genpass  10998  addcompr  11010  mulcompr  11012  distrpr  11017  ltexprlem7  11031  addcomsr  11076  addasssr  11077  mulcomsr  11078  mulasssr  11079  distrsr  11080  indval0  12226  uzssz  12887  uzwo  12939  nn01to3  12969  xnn0xaddcl  13265  elixx3g  13389  iooid  13404  elfz2  13546  injresinjlem  13824  injresinj  13825  fleqceilz  13892  modifeq2int  13974  modfzo0difsn  13984  addmodlteq  13987  ltweuz  14002  fzofi  14015  fsuppmapnn0fiubex  14033  hashrabrsn  14413  hashrabsn01  14414  hashrabsn1  14415  elprchashprn2  14437  hashss  14450  hashsn01  14458  hash1snb  14461  hashgt12el  14464  hashgt12el2  14465  hashgt23el  14466  hashfzp1  14473  hashfundm  14484  hash2pwpr  14518  hashge2el2dif  14522  hash3tpde  14535  ffz0iswrd  14583  ccatsymb  14625  swrd00  14687  swrd0  14701  swrdwrdsymb  14705  pfx00  14717  pfx0  14718  repswswrd  14826  0csh0  14835  cshwcl  14840  cshwidxmod  14845  repswcshw  14854  cshw1  14864  s3sndisj  15009  s3iunsndisj  15010  xptrrel  15022  trclfvcotrg  15058  relexpfld  15091  reusq0  15521  modfsummods  15850  dvdsaddre2b  16369  gcdaddmlem  16586  prm23ge5  16879  pcmptcl  16955  prmgaplem5  17119  prmgaplem6  17120  cshwshash  17168  strle1  17222  strfvss  17251  strfvi  17254  setsnid  17272  ressbas  17300  ressbasssg  17301  ressbasssOLD  17304  resseqnbas  17306  ress0  17307  ressress  17311  0rest  17486  firest  17489  topnval  17491  xpsaddlem  17631  xpsvsca  17635  homffval  17750  comfffval  17758  oppchomfval  17774  oppcbas  17778  fullfunc  17969  fthfunc  17970  natfval  18010  fucbas  18024  fuchom  18025  arwval  18104  coafval  18125  xpcbas  18238  xpchomfval  18239  xpccofval  18242  oduval  18348  oduleval  18349  lubfun  18410  glbfun  18423  odujoin  18466  odumeet  18468  ipopos  18596  plusffval  18708  grpidval  18723  gsum0  18746  frmdplusg  18917  frmd0  18923  efmndbas  18934  efmndbasabf  18935  efmndplusg  18943  mgm2nsgrplem2  18985  mgm2nsgrplem3  18986  sgrp2rid2  18992  dfgrp2e  19034  grpinvfval  19049  grpinvfvalALT  19050  grpinvfvi  19053  grpsubfval  19054  grpsubfvalALT  19055  mulgfval  19139  mulgfvalALT  19140  mulgfvi  19143  cntrval  19393  oppgval  19421  oppgplusfval  19422  symgval  19445  snsymgefmndeq  19469  psgnfval  19574  odfval  19606  odfvalALT  19607  oppglsm  19716  efgval  19791  mgpval  20223  mgpplusg  20224  ringidval  20269  opprval  20425  opprmulfval  20426  dvdsrval  20448  invrfval  20476  dvrfval  20489  rrgval  20805  staffval  20953  scaffval  21010  rlmval  21321  rlmsca2  21329  2idlval  21399  nzerooringczr  21639  zrhval  21666  zlmlem  21675  zlmvsca  21680  chrval  21682  evpmss  21745  psgndiflemB  21759  ipffval  21807  thlbas  21855  thlle  21856  thloc  21858  pjfval  21865  dsmmval2  21895  asclfval  22037  psrplusg  22096  psrmulr  22101  psrvscafval  22107  mplval  22147  mplcoe3  22198  evlval  22260  psr1val  22355  vr1val  22361  ply1val  22363  ply1basfvi  22409  ply1plusgfvi  22410  psr1sca2  22419  ply1sca2  22422  ply1ascl  22428  cply1mul  22465  gsummoncoe1  22477  evl1fval  22497  evl1fval1  22500  mamufacex  22562  mavmulsolcl  22717  marrepfval  22726  marepvfval  22731  submafval  22745  mdetfval  22752  mdetfval1  22756  mdetunilem7  22784  mdetunilem8  22785  madufval  22803  minmar1fval  22812  mp2pm2mplem4  22975  toponsspwpw  23088  tgdif0  23158  indislem  23166  resstopn  23352  iocpnfordt  23381  icomnfordt  23382  hmeofval  23924  ussval  24425  nmfval  24754  nghmfval  24888  pcofval  25178  tcphval  25386  ioombl  25733  ibladdlem  25988  itgaddlem1  25991  iblabs  25997  dvbsss  26070  perfdvf  26071  mdegfval  26228  deg1fval  26246  deg1fvi  26251  uc1pval  26306  mon1pval  26308  2irrexpq  26905  lgsqrmodndvds  27526  gausslemma2dlem1a  27538  2lgs  27580  2sqreultblem  27621  2sqreunnltblem  27624  newval  28037  leftval  28051  rightval  28052  lltr  28064  oldssmade  28069  oldss  28072  lrold  28099  ttglem  29234  axcontlem12  29334  vtxval  29359  iedgval  29360  edgval  29408  usgr1v  29615  nbuhgr  29702  nbumgr  29706  uhgrnbgr0nb  29713  nbgr1vtx  29717  nbgrnself2  29719  nbusgrvtxm1  29738  sizusglecusg  29822  g0wlk0  30009  wlkreslem  30026  lfgrwlkprop  30044  wwlks  30193  wwlksn  30195  wspthsn  30206  iswwlksnon  30211  iswspthsnon  30214  0enwwlksnge1  30222  wwlksnfi  30264  clwwlk  30343  umgrclwwlkge2  30351  clwlkclwwlklem2a4  30357  clwwlkn  30386  clwwlknonmpo  30449  clwwlknon  30450  clwwlk0on0  30452  clwwlknon1le1  30461  1conngr  30554  eupth2lem3lem7  30594  frgr1v  30631  nfrgr2v  30632  1to2vfriswmgr  30639  2wspmdisj  30697  frgrreggt1  30753  frgrreg  30754  frgrregord013  30755  frgrogt3nreg  30757  friendship  30759  avril1  30823  vafval  30964  bafval  30965  smfval  30966  vsfval  30994  bcsiALT  31540  of0r  33033  fracval  33634  fracbas  33635  resvsca  33661  resvlem  33662  cntnevol  34627  signsw0glem  34949  bnj1189  35406  r1wf  35498  rankscottu  35531  noinfepregs  35554  kardval  35573  kard0b  35580  kardcard2b  35586  rankkardu  35592  fmlafvel  35885  gonan0  35892  satffun  35909  mvtval  36000  mexval  36002  mexval2  36003  mdvval  36004  mrsubfval  36008  mrsubrn  36013  msubfval  36024  elmsubrn  36028  msubrn  36029  mvhfval  36033  mpstval  36035  msrfval  36037  mstaval  36044  mppsval  36072  mthmval  36075  antnestlaw2  36192  dfrdg3  36294  fvsingle  36418  unisnif  36423  funpartfv  36445  fullfunfv  36447  linedegen  36643  axtcond  37017  csbttc  37048  mh-setindnd  37076  bj-ax6e  37318  axc11n11r  37336  bj-ax12v3ALT  37339  bj-sbsb  37500  bj-nfcsym  37562  bj-snex  37699  bj-restsnid  37757  bj-inftyexpitaudisj  37877  bj-inftyexpidisj  37882  finxpreclem4  38068  finxp00  38076  isinf2  38079  wl-nfs1t  38220  matunitlindflem1  38295  itg2addnclem  38350  ibladdnclem  38355  itgaddnclem1  38357  iblabsnc  38363  iblmulc2nc  38364  ftc1anclem8  38379  ismgmOLD  38529  tsbi1  38810  tsbi2  38811  ac6s6  38849  equid1  39701  ax12fromc15  39707  equid1ALT  39727  dvelimf-o  39731  ax12inda2ALT  39748  ax12inda2  39749  sn-axprlem3  43017  fsuppind  43350  mzpmfp  43506  itgocn  43919  mendbas  43935  mendplusgfval  43936  mendmulrfval  43938  mendsca  43940  mendvscafval  43941  arearect  43970  areaquad  43971  fpwfvss  44166  safesnsupfidom1o  44171  sn1dom  44280  or3or  44777  uneqsn  44779  addcomgi  45192  ax6e2ndeq  45296  2sb5ndVD  45646  2sb5ndALT  45668  sqwvfoura  46970  sqwvfourb  46971  fourierswlem  46972  fouriersw  46973  hspdifhsp  47358  hspmbllem2  47369  hspmbl  47371  et-ltneverrefl  47613  tz6.12-afv  47938  ndmaovcl  47968  tz6.12-afv2  48005  otiunsndisjX  48044  fvmptrab  48057  nltle2tri  48078  fzopredsuc  48089  iccpartiltu  48199  iccpartigtl  48200  iccpartlt  48201  icceuelpartlem  48212  iccpartnel  48215  elsprel  48252  sprssspr  48258  sprsymrelfvlem  48267  prprelprb  48294  prprspr2  48295  fmtnoprmfac1  48345  fmtnoprmfac2  48347  prmdvdsfmtnof1lem2  48365  prminf2  48368  lighneallem4  48390  requad1  48415  requad2  48416  evenprm2  48507  even3prm2  48512  fpprbasnn  48522  stgoldbwt  48569  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem2lem3  48909  upwlkbprop  48931  pgrpgt2nabl  49174  suppmptcfin  49184  linc1  49233  lindslinindsimp2lem5  49270  1aryenef  49453  2aryenef  49464  reorelicc  49518  rrxsphere  49556  fvconst0ci  49697  fvconstdomi  49698  upfval  49982  reldmprcof1  50187  reldmprcof2  50188  lmdfval  50455  cmdfval  50456  setrec2lem1  50499  setrec2mpt  50503