Theorem pm2.61i 182

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 158	. 2 ⊢ (¬ 𝜓 → 𝜓)
4	3	pm2.18i 129	1 ⊢ 𝜓

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.61ii  183  pm2.61nii  184  pm2.61iii  185  pm2.65i  193  pm5.21nii  379  pm5.18  382  biass  385  pm2.61ian  810  ecase3  1030  4cases  1039  pm4.42  1052  ifpid  1076  elimh  1083  3ecase  1474  norass  1538  ax6e  2381  ax12  2421  exdistrf  2445  equvini  2453  ax12vALT  2467  2ax6e  2469  sb1  2477  sb2  2478  sb1OLD  2480  sb4a  2482  dfsb1  2483  dfsb2  2495  sbcom3  2508  sbco2  2513  sbco3  2515  sb9  2521  nfsbOLD  2526  eujustALT  2570  pm2.61ine  3028  ralcom2  3350  eueq2  3668  moeq3  3670  mo2icl  3672  sbc2or  3748  unineq  4237  csb0  4367  sbcel12  4368  sbcne12  4372  sbcel2  4375  csbidm  4390  csbun  4398  csbin  4399  ralidmOLD  4473  csbdif  4485  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  4680  rabsnif  4684  tppreqb  4765  ssunsn2  4787  n0snor2el  4791  preq12nebg  4820  opthprneg  4822  elpreqprlem  4823  dfopif  4827  csbuni  4897  disjord  5093  sbcbr  5160  unisn2  5269  intabs  5299  class2set  5310  dtruALT2  5325  snexALT  5338  dtruALT  5343  axprlem3  5380  snex  5388  exneq  5392  dtruOLD  5398  copsexgw  5447  copsexg  5448  snopeqop  5463  csbopab  5512  0nelopabOLD  5525  dfid3  5534  csbxp  5731  csbres  5940  csbima12  6031  soirri  6080  csbrn  6155  dmsnopss  6166  dmsnsnsn  6172  opswap  6181  unixpid  6236  predres  6293  nsuceq0  6400  ordsssuc2  6408  iotassuni  6468  iotaex  6469  iotassuniOLD  6475  iotaexOLD  6476  csbiota  6489  dffv3  6838  fvrn0  6872  ndmfv  6877  elfv2ex  6888  fveqres  6889  csbfv12  6890  csbfv  6892  dffv2  6936  fvco4i  6942  fvmptss  6960  fvmptex  6962  fvmptss2  6973  fvmptrabfv  6979  f0cli  7047  fvunsn  7124  fconst5  7154  csbriota  7328  riotassuni  7353  oprabidw  7387  csbov123  7398  csbov  7399  fvmptopab  7410  fvmptopabOLD  7411  brfvopab  7413  elimdelov  7452  ovif12  7455  ndmovcl  7538  ndmovord  7543  elovmpt3imp  7609  difsnexi  7694  ordsuc  7747  ordsucOLD  7748  ordsucelsuc  7756  1stval  7922  2ndval  7923  1st2val  7948  2nd2val  7949  el2mpocsbcl  8016  bropopvvv  8021  bropfvvvvlem  8022  bropfvvvv  8023  suppimacnv  8104  suppssdm  8107  ressuppss  8113  suppun  8114  extmptsuppeq  8118  funsssuppss  8120  fczsupp0  8123  suppss  8124  suppssOLD  8125  suppssov1  8128  suppss2  8130  suppssfv  8132  suppco  8136  mpoxopynvov0  8148  mpoxopoveqd  8151  pwuninel  8205  smofvon2  8301  om0x  8464  mapssfset  8788  brdomg  8895  brdomgOLD  8896  snfi  8987  sdomirr  9057  domunsn  9070  2pwuninel  9075  unfi  9115  cnvfi  9123  snnen2oOLD  9170  suppeqfsuppbi  9318  fsuppun  9323  funsnfsupp  9328  fipwuni  9361  oicl  9464  oif  9465  wemapso2  9488  card2on  9489  en2lp  9541  ttrclselem1  9660  tctr  9675  r1tr  9711  rankdmr1  9736  r1pw  9780  r1pwALT  9781  rankuni  9798  scottex  9820  cardidm  9894  alephcard  10005  alephnbtwn  10006  cfub  10184  cardcf  10187  cflecard  10188  cfle  10189  cflim2  10198  cfidm  10210  isf32lem9  10296  itunisuc  10354  itunitc1  10355  itunitc  10356  ituniiun  10357  axcc2lem  10371  alephreg  10517  pwcfsdom  10518  cfpwsdom  10519  axunndlem1  10530  axpownd  10536  tskmcl  10776  addcompi  10829  addasspi  10830  mulcompi  10831  mulasspi  10832  distrpi  10833  addnidpi  10836  nlt1pi  10841  addcompq  10885  addcomnq  10886  mulcompq  10887  mulcomnq  10888  adderpq  10891  mulerpq  10892  addassnq  10893  mulassnq  10894  distrnq  10896  genpass  10944  addcompr  10956  mulcompr  10958  distrpr  10963  ltexprlem7  10977  addcomsr  11022  addasssr  11023  mulcomsr  11024  mulasssr  11025  distrsr  11026  uzssz  12783  uzwo  12835  nn01to3  12865  xnn0xaddcl  13153  elixx3g  13276  iooid  13291  elfz2  13430  injresinjlem  13691  injresinj  13692  fleqceilz  13758  modifeq2int  13837  modfzo0difsn  13847  addmodlteq  13850  ltweuz  13865  fzofi  13878  fsuppmapnn0fiubex  13896  hashrabrsn  14271  hashrabsn01  14272  hashrabsn1  14273  elprchashprn2  14295  hashss  14308  hashsn01  14315  hash1snb  14318  hashgt12el  14321  hashgt12el2  14322  hashgt23el  14323  hashfzp1  14330  hash2pwpr  14374  hashge2el2dif  14378  ffz0iswrd  14428  ccatsymb  14469  swrd00  14531  swrd0  14545  swrdwrdsymb  14549  pfx00  14561  pfx0  14562  repswswrd  14671  0csh0  14680  cshwcl  14685  cshwidxmod  14690  repswcshw  14699  cshw1  14709  s3sndisj  14851  s3iunsndisj  14852  xptrrel  14864  trclfvcotrg  14900  relexpfld  14933  reusq0  15346  modfsummods  15677  dvdsaddre2b  16188  gcdaddmlem  16403  prm23ge5  16686  pcmptcl  16762  prmgaplem5  16926  prmgaplem6  16927  cshwshash  16976  strle1  17029  strfvss  17058  strfvi  17061  setsnid  17080  setsnidOLD  17081  ressbas  17117  ressbasOLD  17118  ressbasss  17120  resseqnbas  17121  resslemOLD  17122  ress0  17123  ressress  17128  0rest  17310  firest  17313  topnval  17315  xpsaddlem  17454  xpsvsca  17458  homffval  17569  comfffval  17577  oppchomfval  17593  oppchomfvalOLD  17594  oppcbas  17598  oppcbasOLD  17599  fullfunc  17792  fthfunc  17793  natfval  17832  fucbas  17847  fuchom  17848  fuchomOLD  17849  arwval  17928  coafval  17949  xpcbas  18065  xpchomfval  18066  xpccofval  18069  oduval  18176  oduleval  18177  lubfun  18240  glbfun  18253  odujoin  18296  odumeet  18298  ipopos  18424  plusffval  18502  grpidval  18515  gsum0  18538  frmdplusg  18663  frmd0  18669  efmndbas  18680  efmndbasabf  18681  efmndplusg  18689  mgm2nsgrplem2  18728  mgm2nsgrplem3  18729  sgrp2rid2  18735  dfgrp2e  18775  grpinvfval  18788  grpinvfvalALT  18789  grpinvfvi  18792  grpsubfval  18793  grpsubfvalALT  18794  mulgfval  18872  mulgfvalALT  18873  mulgfvi  18876  cntrval  19097  oppgval  19123  oppgplusfval  19124  symgval  19148  snsymgefmndeq  19174  psgnfval  19280  odfval  19312  odfvalALT  19313  oppglsm  19422  efgval  19497  mgpval  19897  mgpplusg  19898  ringidval  19913  opprval  20048  opprmulfval  20049  dvdsrval  20072  invrfval  20100  dvrfval  20111  staffval  20304  scaffval  20338  rlmval  20658  rlmsca2  20668  2idlval  20701  rrgval  20755  zrhval  20906  zlmlem  20915  zlmlemOLD  20916  zlmvsca  20924  chrval  20926  evpmss  20988  psgndiflemB  21002  ipffval  21050  thlbas  21098  thlbasOLD  21099  thlle  21100  thlleOLD  21101  thloc  21103  pjfval  21110  dsmmval2  21140  asclfval  21280  psrplusg  21347  psrmulr  21350  psrvscafval  21356  mplval  21395  mplcoe3  21437  evlval  21503  psr1val  21555  vr1val  21561  ply1val  21563  ply1basfvi  21610  ply1plusgfvi  21611  psr1sca2  21620  ply1sca2  21623  ply1ascl  21627  cply1mul  21663  gsummoncoe1  21673  evl1fval  21692  evl1fval1  21695  mamufacex  21736  mavmulsolcl  21898  marrepfval  21907  marepvfval  21912  submafval  21926  mdetfval  21933  mdetfval1  21937  mdetunilem7  21965  mdetunilem8  21966  madufval  21984  minmar1fval  21993  mp2pm2mplem4  22156  toponsspwpw  22269  tgdif0  22340  indislem  22348  resstopn  22535  iocpnfordt  22564  icomnfordt  22565  hmeofval  23107  ussval  23609  nmfval  23942  nghmfval  24084  pcofval  24371  tcphval  24580  ioombl  24927  ibladdlem  25182  itgaddlem1  25185  iblabs  25191  dvbsss  25264  perfdvf  25265  mdegfval  25425  deg1fval  25443  deg1fvi  25448  uc1pval  25502  mon1pval  25504  2irrexpq  26083  lgsqrmodndvds  26699  gausslemma2dlem1a  26711  2lgs  26753  2sqreultblem  26794  2sqreunnltblem  26797  newval  27183  leftval  27191  rightval  27192  oldssmade  27205  lrold  27224  ttglem  27766  ttglemOLD  27767  axcontlem12  27871  vtxval  27898  iedgval  27899  edgval  27947  usgr1v  28151  nbuhgr  28238  nbumgr  28242  uhgrnbgr0nb  28249  nbgr1vtx  28253  nbgrnself2  28255  nbusgrvtxm1  28274  sizusglecusg  28358  g0wlk0  28547  wlkreslem  28564  lfgrwlkprop  28582  wwlks  28727  wwlksn  28729  wspthsn  28740  iswwlksnon  28745  iswspthsnon  28748  0enwwlksnge1  28756  wwlksnfi  28798  clwwlk  28874  umgrclwwlkge2  28882  clwlkclwwlklem2a4  28888  clwwlkn  28917  clwwlknonmpo  28980  clwwlknon  28981  clwwlk0on0  28983  clwwlknon1le1  28992  1conngr  29085  eupth2lem3lem7  29125  frgr1v  29162  nfrgr2v  29163  1to2vfriswmgr  29170  2wspmdisj  29228  frgrreggt1  29284  frgrreg  29285  frgrregord013  29286  frgrogt3nreg  29288  friendship  29290  avril1  29354  vafval  29492  bafval  29493  smfval  29494  vsfval  29522  bcsiALT  30068  resvsca  32065  resvlem  32066  resvlemOLD  32067  cntnevol  32767  signsw0glem  33105  bnj1189  33561  hashfundm  33646  fmlafvel  33919  gonan0  33926  satffun  33943  mvtval  34034  mexval  34036  mexval2  34037  mdvval  34038  mrsubfval  34042  mrsubrn  34047  msubfval  34058  elmsubrn  34062  msubrn  34063  mvhfval  34067  mpstval  34069  msrfval  34071  mstaval  34078  mppsval  34106  mthmval  34109  dfrdg3  34311  fvsingle  34495  unisnif  34500  funpartfv  34520  fullfunfv  34522  linedegen  34718  bj-ax6e  35122  axc11n11r  35138  bj-ax12v3ALT  35141  bj-sbsb  35292  bj-nfcsym  35356  bj-snex  35496  bj-restsnid  35548  bj-inftyexpitaudisj  35666  bj-inftyexpidisj  35671  finxpreclem4  35855  finxp00  35863  isinf2  35866  wl-nfs1t  35986  matunitlindflem1  36064  itg2addnclem  36119  ibladdnclem  36124  itgaddnclem1  36126  iblabsnc  36132  iblmulc2nc  36133  ftc1anclem8  36148  ismgmOLD  36299  tsbi1  36582  tsbi2  36583  ac6s6  36621  equid1  37351  ax12fromc15  37357  equid1ALT  37377  dvelimf-o  37381  ax12inda2ALT  37398  ax12inda2  37399  sn-axprlem3  40628  ressbasssg  40658  fsuppind  40742  mzpmfp  41047  itgocn  41468  mendbas  41488  mendplusgfval  41489  mendmulrfval  41491  mendsca  41493  mendvscafval  41494  arearect  41526  areaquad  41527  fpwfvss  41665  safesnsupfidom1o  41670  sn1dom  41779  or3or  42276  uneqsn  42278  addcomgi  42717  ax6e2ndeq  42822  2sb5ndVD  43173  2sb5ndALT  43195  sqwvfoura  44440  sqwvfourb  44441  fourierswlem  44442  fouriersw  44443  hspdifhsp  44828  hspmbllem2  44839  hspmbl  44841  et-ltneverrefl  45083  tz6.12-afv  45376  ndmaovcl  45406  tz6.12-afv2  45443  otiunsndisjX  45482  fvmptrab  45495  nltle2tri  45516  fzopredsuc  45526  iccpartiltu  45585  iccpartigtl  45586  iccpartlt  45587  icceuelpartlem  45598  iccpartnel  45601  elsprel  45638  sprssspr  45644  sprsymrelfvlem  45653  prprelprb  45680  prprspr2  45681  fmtnoprmfac1  45728  fmtnoprmfac2  45730  prmdvdsfmtnof1lem2  45748  prminf2  45751  lighneallem4  45773  requad1  45785  requad2  45786  evenprm2  45877  even3prm2  45882  fpprbasnn  45892  stgoldbwt  45939  upwlkbprop  46011  nzerooringczr  46341  pgrpgt2nabl  46413  suppmptcfin  46426  linc1  46477  lindslinindsimp2lem5  46514  1aryenef  46702  2aryenef  46713  reorelicc  46767  rrxsphere  46805  fvconst0ci  46896  fvconstdomi  46897  setrec2lem1  47109  setrec2mpt  47113