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  824  ecase3  1048  4cases  1056  pm4.42  1069  ifpid  1093  elimh  1099  3ecase  1506  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  3042  ralcom2  3366  eueq2  3671  moeq3  3673  mo2icl  3675  sbc2or  3751  unineq  4236  csb0  4371  sbcel12  4372  sbcne12  4376  sbcel2  4379  csbidm  4394  csbun  4402  csbin  4403  csbdif  4484  ifsb  4499  ifid  4526  ifnot  4538  ifan  4539  ifor  4540  csbif  4543  elimhyp  4551  elimhyp2v  4552  elimhyp3v  4553  elimhyp4v  4554  elimdhyp  4556  keephyp2v  4558  keephyp3v  4559  rmosn  4682  rabsnif  4686  tppreqb  4770  ssunsn2  4788  n0snor2el  4793  preq12nebg  4823  opthprneg  4825  elpreqprlem  4826  dfopif  4842  csbuni  4903  disjord  5097  sbcbr  5167  unisn2  5272  intabs  5317  class2set  5323  dtruALT2  5339  snexALT  5352  dtruALT  5357  axprlem3  5394  axprglem  5401  axprg  5402  snexOLD  5407  exneq  5411  copsexgwOLD  5468  copsexg  5469  snopeqop  5485  csbopab  5537  dfid3  5556  csbxp  5760  csbcnv  5876  csbres  5989  csbima12  6094  soirri  6138  csbrn  6223  dmsnopss  6234  dmsnsnsn  6240  opswap  6249  unixpid  6311  predres  6368  nsuceq0  6474  ordsssuc2  6482  iotassuni  6540  iotaex  6541  csbiota  6559  dffv3  6912  fvrn0  6944  ndmfv  6948  elfv2ex  6959  fveqres  6960  csbfv12  6961  csbfv  6963  dffv2  7011  fvco4i  7018  fvmptss  7037  fvmptex  7039  fvmptss2  7051  fvmptrabfv  7057  f0cli  7130  fvunsn  7215  fconst5  7243  csbriota  7423  riotassuni  7448  oprabidw  7482  csbov123  7495  csbov  7496  fvmptopab  7506  brfvopab  7508  elimdelov  7547  ovif12  7551  ifmpt2v  7553  ndmovcl  7638  ndmovord  7643  elovmpt3imp  7710  difsnexi  7807  ordsuc  7859  ordsucelsuc  7867  1stval  8037  2ndval  8038  1st2val  8063  2nd2val  8064  el2mpocsbcl  8131  bropopvvv  8136  bropfvvvvlem  8137  bropfvvvv  8138  suppimacnv  8229  suppssdm  8232  ressuppss  8238  suppun  8239  extmptsuppeq  8243  funsssuppss  8245  fczsupp0  8248  suppss  8249  suppss2  8255  suppssfv  8257  suppco  8261  mpoxopynvov0  8273  mpoxopoveqd  8276  pwuninelOLD  8331  smofvon2  8402  om0x  8565  mapssfset  8911  brdomg  9023  snfi  9109  sdomirr  9171  domunsn  9184  2pwuninel  9189  unfi  9224  cnvfi  9229  suppeqfsuppbi  9408  fsuppun  9416  funsnfsupp  9421  fipwuni  9455  oicl  9560  oif  9561  wemapso2  9584  card2on  9585  en2lp  9644  ttrclselem1  9763  tctr  9776  r1tr  9820  rankdmr1  9846  r1wf  9878  r1pw  9896  r1pwALT  9897  rankuni  9916  scottex  9970  scottexOLD  9971  setrec2lem1  10011  cardidm  10077  alephcard  10188  alephnbtwn  10189  cfub  10365  cardcf  10368  cflecard  10369  cfle  10370  cflim2  10380  cfidm  10392  isf32lem9  10478  itunisuc  10536  itunitc1  10537  itunitc  10538  ituniiun  10539  axcc2lem  10553  alephreg  10706  pwcfsdom  10707  cfpwsdom  10708  axunndlem1  10719  axpownd  10725  tskmcl  10965  addcompi  11018  addasspi  11019  mulcompi  11020  mulasspi  11021  distrpi  11022  addnidpi  11025  nlt1pi  11030  addcompq  11074  addcomnq  11075  mulcompq  11076  mulcomnq  11077  adderpq  11080  mulerpq  11081  addassnq  11082  mulassnq  11083  distrnq  11085  genpass  11133  addcompr  11145  mulcompr  11147  distrpr  11152  ltexprlem7  11166  addcomsr  11211  addasssr  11212  mulcomsr  11213  mulasssr  11214  distrsr  11215  indval0  12364  uzssz  13026  uzwo  13078  nn01to3  13108  xnn0xaddcl  13405  elixx3g  13529  iooid  13544  elfz2  13686  injresinjlem  13965  injresinj  13966  fleqceilz  14034  modifeq2int  14116  modfzo0difsn  14126  addmodlteq  14129  ltweuz  14144  fzofi  14157  fsuppmapnn0fiubex  14175  hashrabrsn  14557  hashrabsn01  14558  hashrabsn1  14559  elprchashprn2  14581  hashss  14594  hashsn01  14602  hash1snb  14605  hashgt12el  14608  hashgt12el2  14609  hashgt23el  14610  hashfzp1  14617  hashfundm  14628  hash2pwpr  14662  hashge2el2dif  14666  hash3tpde  14679  ffz0iswrd  14727  ccatsymb  14769  swrd00  14834  swrd0  14850  swrdwrdsymb  14854  pfx00  14866  pfx0  14867  repswswrd  14977  0csh0  14986  cshwcl  14991  cshwidxmod  14996  repswcshw  15005  cshw1  15015  s3sndisj  15163  s3iunsndisj  15164  xptrrel  15176  trclfvcotrg  15212  relexpfld  15245  reusq0  15676  modfsummods  16004  dvdsaddre2b  16521  gcdaddmlem  16740  prm23ge5  17037  pcmptcl  17113  prmgaplem5  17277  prmgaplem6  17278  cshwshash  17326  strle1  17380  strfvss  17409  strfvi  17412  setsnid  17430  ressbas  17458  ressbasssg  17459  ressbasssOLD  17462  resseqnbas  17464  ress0  17465  ressress  17469  0rest  17650  firest  17653  topnval  17655  xpsaddlem  17795  xpsvsca  17799  homffval  17914  comfffval  17922  oppchomfval  17938  oppcbas  17942  fullfunc  18133  fthfunc  18134  natfval  18174  fucbas  18188  fuchom  18189  arwval  18268  coafval  18289  xpcbas  18402  xpchomfval  18403  xpccofval  18406  oduval  18512  oduleval  18513  lubfun  18574  glbfun  18587  odujoin  18630  odumeet  18632  ipopos  18760  plusffval  18872  grpidval  18890  gsum0  18923  frmdplusg  19100  frmd0  19106  efmndbas  19117  efmndbasabf  19118  efmndplusg  19126  mgm2nsgrplem2  19168  mgm2nsgrplem3  19169  sgrp2rid2  19175  dfgrp2e  19224  grpinvfval  19239  grpinvfvalALT  19240  grpinvfvi  19243  grpsubfval  19244  grpsubfvalALT  19245  mulgfval  19329  mulgfvalALT  19330  mulgfvi  19333  cntrval  19584  oppgval  19612  oppgplusfval  19613  symgval  19636  snsymgefmndeq  19660  psgnfval  19765  odfval  19797  odfvalALT  19798  oppglsm  19907  efgval  19982  mgpval  20414  mgpplusg  20415  ringidval  20460  opprval  20619  opprmulfval  20620  dvdsrval  20642  invrfval  20670  dvrfval  20683  rrgval  21000  staffval  21149  scaffval  21206  rlmval  21517  rlmsca2  21525  2idlval  21595  nzerooringczr  21841  zrhval  21868  zlmlem  21877  zlmvsca  21882  chrval  21884  evpmss  21947  psgndiflemB  21961  ipffval  22009  thlbas  22057  thlle  22058  thloc  22060  pjfval  22067  dsmmval2  22097  asclfval  22241  psrplusg  22300  psrmulr  22305  psrvscafval  22311  mplval  22351  mplcoe3  22402  evlval  22464  psr1val  22559  vr1val  22565  ply1val  22567  ply1basfvi  22613  ply1plusgfvi  22614  psr1sca2  22623  ply1sca2  22626  ply1ascl  22632  cply1mul  22669  gsummoncoe1  22681  evl1fval  22701  evl1fval1  22704  mamufacex  22766  mavmulsolcl  22921  marrepfval  22930  marepvfval  22935  submafval  22949  mdetfval  22956  mdetfval1  22960  mdetunilem7  22988  mdetunilem8  22989  madufval  23007  minmar1fval  23016  matunitlindflem1  23049  mp2pm2mplem4  23182  toponsspwpw  23295  tgdif0  23365  indislem  23373  resstopn  23559  iocpnfordt  23588  icomnfordt  23589  hmeofval  24132  ussval  24633  nmfval  24962  nghmfval  25096  pcofval  25386  tcphval  25594  ioombl  25941  ibladdlem  26195  itgaddlem1  26198  iblabs  26204  dvbsss  26277  perfdvf  26278  mdegfval  26435  deg1fval  26453  deg1fvi  26458  uc1pval  26513  mon1pval  26515  2irrexpq  27116  lgsqrmodndvds  27737  gausslemma2dlem1a  27749  2lgs  27791  2sqreultblem  27832  2sqreunnltblem  27835  newval  28278  leftval  28292  rightval  28293  lltr  28305  oldssmade  28310  oldss  28313  lrold  28340  ttglem  29510  axcontlem12  29610  vtxval  29635  iedgval  29636  edgval  29684  usgr1v  29894  nbuhgr  29981  nbumgr  29985  uhgrnbgr0nb  29992  nbgr1vtx  29996  nbgrnself2  29998  nbusgrvtxm1  30017  sizusglecusg  30101  g0wlk0  30288  wlkreslem  30305  lfgrwlkprop  30327  wwlks  30481  wwlksn  30483  wspthsn  30494  iswwlksnon  30499  iswspthsnon  30502  0enwwlksnge1  30510  wwlksnfi  30552  clwwlk  30631  umgrclwwlkge2  30639  clwlkclwwlklem2a4  30645  clwwlkn  30674  clwwlknonmpo  30737  clwwlknon  30738  clwwlk0on0  30740  clwwlknon1le1  30749  1conngr  30852  eupth2lem3lem7  30892  frgr1v  30929  nfrgr2v  30930  1to2vfriswmgr  30937  2wspmdisj  30995  frgrreggt1  31051  frgrreg  31052  frgrregord013  31053  frgrogt3nreg  31055  friendship  31057  avril1  31121  vafval  31262  bafval  31263  smfval  31264  vsfval  31292  bcsiALT  31838  of0r  33370  fracval  33970  fracbas  33971  resvsca  33997  resvlem  33998  cntnevol  34972  signsw0glem  35293  bnj1189  35750  rankscottu  35880  noinfepregs  35942  kardval  35961  kard0b  35968  kardcard2b  35974  rankkardu  35980  j0ltaleph  36049  k1on  36056  k2on  36057  k39o  36058  fmlafvel  36358  gonan0  36365  satffun  36382  mvtval  36473  mexval  36475  mexval2  36476  mdvval  36477  mrsubfval  36481  mrsubrn  36486  msubfval  36497  elmsubrn  36501  msubrn  36502  mvhfval  36506  mpstval  36508  msrfval  36510  mstaval  36517  mppsval  36545  mthmval  36548  antnestlaw2  36665  dfrdg3  36773  fvsingle  36897  unisnif  36902  funpartfv  36924  fullfunfv  36926  linedegen  37123  axtcond  37481  csbttc  37512  mh-setindnd  37540  bj-ax6e  37782  axc11n11r  37800  bj-ax12v3ALT  37803  bj-sbsb  37964  bj-nfcsym  38026  bj-snex  38163  bj-restsnid  38278  bj-inftyexpitaudisj  38394  bj-inftyexpidisj  38399  finxpreclem4  38585  finxp00  38593  isinf2  38596  wl-nfs1t  38737  itg2addnclem  38857  ibladdnclem  38862  itgaddnclem1  38864  iblabsnc  38870  iblmulc2nc  38871  ftc1anclem8  38886  ismgmOLD  39050  tsbi1  39331  tsbi2  39332  ac6s6  39370  equid1  40222  ax12fromc15  40228  equid1ALT  40248  dvelimf-o  40252  ax12inda2ALT  40269  ax12inda2  40270  sn-axprlem3  43539  fsuppind  43884  mzpmfp  44024  itgocn  44431  mendbas  44443  mendplusgfval  44444  mendmulrfval  44446  mendsca  44448  mendvscafval  44449  arearect  44478  areaquad  44479  fpwfvss  44674  safesnsupfidom1o  44679  sn1dom  44788  or3or  45284  uneqsn  45286  addcomgi  45698  ax6e2ndeq  45802  2sb5ndVD  46152  2sb5ndALT  46174  sqwvfoura  47511  sqwvfourb  47512  fourierswlem  47513  fouriersw  47514  hspdifhsp  47899  hspmbllem2  47910  hspmbl  47912  et-ltneverrefl  48154  aiotaexim  48441  tz6.12-afv  48516  ndmaovcl  48546  tz6.12-afv2  48583  otiunsndisjX  48622  fvmptrab  48635  nltle2tri  48656  fzopredsuc  48667  iccpartiltu  48777  iccpartigtl  48778  iccpartlt  48779  icceuelpartlem  48790  iccpartnel  48793  elsprel  48830  sprssspr  48836  sprsymrelfvlem  48845  prprelprb  48872  prprspr2  48873  fmtnoprmfac1  48923  fmtnoprmfac2  48925  prmdvdsfmtnof1lem2  48943  prminf2  48946  lighneallem4  48968  requad1  48993  requad2  48994  evenprm2  49085  even3prm2  49090  fpprbasnn  49100  stgoldbwt  49147  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  upwlkbprop  49509  pgrpgt2nabl  49809  suppmptcfin  49819  linc1  49868  lindslinindsimp2lem5  49905  1aryenef  50088  2aryenef  50099  reorelicc  50153  rrxsphere  50191  fvconst0ci  50336  fvconstdomi  50337  upfval  50623  reldmprcof1  50847  reldmprcof2  50848  lmdfval  51163  cmdfval  51164  setrec2mpt  51196