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 ⊢ 𝜓

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  185  pm2.61nii  186  pm2.61iii  187  pm2.65iOLD  197  pm5.21nii  381  pm5.18  384  biass  388  pm2.61ian  823  ecase3  1046  4cases  1054  pm4.42  1067  ifpid  1091  elimh  1097  3ecase  1502  norass  1564  ax6e  2421  ax12  2461  exdistrf  2485  equvini  2493  ax12vALT  2507  2ax6e  2509  sb1  2516  sb2  2517  sb4a  2518  dfsb1  2519  dfsb2  2531  sbcom3  2544  sbco2  2549  sbco3  2551  sb9  2557  eujustALT  2606  pm2.61ine  3047  ralcom2  3373  eueq2  3682  moeq3  3684  mo2icl  3686  sbc2or  3762  unineq  4249  csb0  4381  sbcel12  4382  sbcne12  4386  sbcel2  4389  csbidm  4404  csbun  4412  csbin  4413  csbdif  4491  ifsb  4506  ifid  4533  ifnot  4545  ifan  4546  ifor  4547  csbif  4550  elimhyp  4558  elimhyp2v  4559  elimhyp3v  4560  elimhyp4v  4561  elimdhyp  4563  keephyp2v  4565  keephyp3v  4566  rmosn  4690  rabsnif  4694  tppreqb  4777  ssunsn2  4797  n0snor2el  4802  preq12nebg  4832  opthprneg  4834  elpreqprlem  4835  dfopif  4839  csbuni  4907  disjord  5102  sbcbr  5170  unisn2  5277  intabs  5320  class2set  5326  dtruALT2  5342  snexALT  5355  dtruALT  5360  axprlem3  5397  axprlem3OLD  5401  axprglem  5408  axprg  5409  snexOLD  5414  exneq  5418  copsexgwOLD  5474  copsexg  5475  snopeqop  5490  csbopab  5541  dfid3  5560  csbxp  5763  csbcnv  5873  csbres  5982  csbima12  6082  soirri  6127  csbrn  6205  dmsnopss  6216  dmsnsnsn  6222  opswap  6231  unixpid  6286  predres  6341  nsuceq0  6447  ordsssuc2  6455  iotassuni  6512  iotaex  6513  csbiota  6530  dffv3  6878  fvrn0  6910  ndmfv  6914  elfv2ex  6925  fveqres  6926  csbfv12  6927  csbfv  6929  dffv2  6977  fvco4i  6984  fvmptss  7003  fvmptex  7005  fvmptss2  7017  fvmptrabfv  7023  f0cli  7094  fvunsn  7178  fconst5  7205  csbriota  7383  riotassuni  7408  oprabidw  7442  csbov123  7455  csbov  7456  fvmptopab  7466  brfvopab  7468  elimdelov  7507  ovif12  7511  ifmpt2v  7513  ndmovcl  7596  ndmovord  7601  elovmpt3imp  7668  difsnexi  7759  ordsuc  7809  ordsucelsuc  7817  1stval  7987  2ndval  7988  1st2val  8013  2nd2val  8014  el2mpocsbcl  8079  bropopvvv  8084  bropfvvvvlem  8085  bropfvvvv  8086  suppimacnv  8169  suppssdm  8172  ressuppss  8178  suppun  8179  extmptsuppeq  8183  funsssuppss  8185  fczsupp0  8188  suppss  8189  suppss2  8195  suppssfv  8197  suppco  8201  mpoxopynvov0  8213  mpoxopoveqd  8216  pwuninelOLD  8271  smofvon2  8342  om0x  8503  mapssfset  8847  brdomg  8954  snfi  9039  sdomirr  9101  domunsn  9114  2pwuninel  9119  unfi  9154  cnvfi  9159  suppeqfsuppbi  9338  fsuppun  9346  funsnfsupp  9351  fipwuni  9385  oicl  9490  oif  9491  wemapso2  9514  card2on  9515  en2lp  9574  ttrclselem1  9693  tctr  9706  r1tr  9747  rankdmr1  9772  r1pw  9816  r1pwALT  9817  rankuni  9834  scottex  9858  cardidm  9944  alephcard  10053  alephnbtwn  10054  cfub  10231  cardcf  10234  cflecard  10235  cfle  10236  cflim2  10246  cfidm  10258  isf32lem9  10344  itunisuc  10402  itunitc1  10403  itunitc  10404  ituniiun  10405  axcc2lem  10419  alephreg  10566  pwcfsdom  10567  cfpwsdom  10568  axunndlem1  10579  axpownd  10585  tskmcl  10825  addcompi  10878  addasspi  10879  mulcompi  10880  mulasspi  10881  distrpi  10882  addnidpi  10885  nlt1pi  10890  addcompq  10934  addcomnq  10935  mulcompq  10936  mulcomnq  10937  adderpq  10940  mulerpq  10941  addassnq  10942  mulassnq  10943  distrnq  10945  genpass  10993  addcompr  11005  mulcompr  11007  distrpr  11012  ltexprlem7  11026  addcomsr  11071  addasssr  11072  mulcomsr  11073  mulasssr  11074  distrsr  11075  indval0  12221  uzssz  12882  uzwo  12934  nn01to3  12964  xnn0xaddcl  13260  elixx3g  13384  iooid  13399  elfz2  13541  injresinjlem  13818  injresinj  13819  fleqceilz  13886  modifeq2int  13968  modfzo0difsn  13978  addmodlteq  13981  ltweuz  13996  fzofi  14009  fsuppmapnn0fiubex  14027  hashrabrsn  14407  hashrabsn01  14408  hashrabsn1  14409  elprchashprn2  14431  hashss  14444  hashsn01  14452  hash1snb  14455  hashgt12el  14458  hashgt12el2  14459  hashgt23el  14460  hashfzp1  14467  hashfundm  14478  hash2pwpr  14512  hashge2el2dif  14516  hash3tpde  14529  ffz0iswrd  14577  ccatsymb  14619  swrd00  14681  swrd0  14695  swrdwrdsymb  14699  pfx00  14711  pfx0  14712  repswswrd  14820  0csh0  14829  cshwcl  14834  cshwidxmod  14839  repswcshw  14848  cshw1  14858  s3sndisj  15003  s3iunsndisj  15004  xptrrel  15016  trclfvcotrg  15052  relexpfld  15085  reusq0  15515  modfsummods  15844  dvdsaddre2b  16364  gcdaddmlem  16581  prm23ge5  16874  pcmptcl  16950  prmgaplem5  17114  prmgaplem6  17115  cshwshash  17163  strle1  17217  strfvss  17246  strfvi  17249  setsnid  17267  ressbas  17295  ressbasssg  17296  ressbasssOLD  17299  resseqnbas  17301  ress0  17302  ressress  17306  0rest  17481  firest  17484  topnval  17486  xpsaddlem  17626  xpsvsca  17630  homffval  17745  comfffval  17753  oppchomfval  17769  oppcbas  17773  fullfunc  17964  fthfunc  17965  natfval  18005  fucbas  18019  fuchom  18020  arwval  18099  coafval  18120  xpcbas  18233  xpchomfval  18234  xpccofval  18237  oduval  18343  oduleval  18344  lubfun  18405  glbfun  18418  odujoin  18461  odumeet  18463  ipopos  18591  plusffval  18703  grpidval  18718  gsum0  18741  frmdplusg  18912  frmd0  18918  efmndbas  18929  efmndbasabf  18930  efmndplusg  18938  mgm2nsgrplem2  18980  mgm2nsgrplem3  18981  sgrp2rid2  18987  dfgrp2e  19029  grpinvfval  19044  grpinvfvalALT  19045  grpinvfvi  19048  grpsubfval  19049  grpsubfvalALT  19050  mulgfval  19134  mulgfvalALT  19135  mulgfvi  19138  cntrval  19388  oppgval  19416  oppgplusfval  19417  symgval  19440  snsymgefmndeq  19464  psgnfval  19569  odfval  19601  odfvalALT  19602  oppglsm  19711  efgval  19786  mgpval  20218  mgpplusg  20219  ringidval  20264  opprval  20419  opprmulfval  20420  dvdsrval  20442  invrfval  20470  dvrfval  20483  rrgval  20781  staffval  20921  scaffval  20978  rlmval  21289  rlmsca2  21297  2idlval  21360  nzerooringczr  21598  zrhval  21625  zlmlem  21634  zlmvsca  21639  chrval  21641  evpmss  21704  psgndiflemB  21718  ipffval  21766  thlbas  21814  thlle  21815  thloc  21817  pjfval  21824  dsmmval2  21854  asclfval  21996  psrplusg  22055  psrmulr  22060  psrvscafval  22066  mplval  22106  mplcoe3  22157  evlval  22219  psr1val  22314  vr1val  22320  ply1val  22322  ply1basfvi  22368  ply1plusgfvi  22369  psr1sca2  22378  ply1sca2  22381  ply1ascl  22387  cply1mul  22424  gsummoncoe1  22436  evl1fval  22456  evl1fval1  22459  mamufacex  22521  mavmulsolcl  22676  marrepfval  22685  marepvfval  22690  submafval  22704  mdetfval  22711  mdetfval1  22715  mdetunilem7  22743  mdetunilem8  22744  madufval  22762  minmar1fval  22771  mp2pm2mplem4  22934  toponsspwpw  23047  tgdif0  23117  indislem  23125  resstopn  23311  iocpnfordt  23340  icomnfordt  23341  hmeofval  23883  ussval  24384  nmfval  24713  nghmfval  24847  pcofval  25137  tcphval  25345  ioombl  25692  ibladdlem  25947  itgaddlem1  25950  iblabs  25956  dvbsss  26029  perfdvf  26030  mdegfval  26187  deg1fval  26205  deg1fvi  26210  uc1pval  26265  mon1pval  26267  2irrexpq  26861  lgsqrmodndvds  27482  gausslemma2dlem1a  27494  2lgs  27536  2sqreultblem  27577  2sqreunnltblem  27580  newval  27993  leftval  28007  rightval  28008  lltr  28020  oldssmade  28025  oldss  28028  lrold  28055  ttglem  29165  axcontlem12  29265  vtxval  29290  iedgval  29291  edgval  29339  usgr1v  29546  nbuhgr  29633  nbumgr  29637  uhgrnbgr0nb  29644  nbgr1vtx  29648  nbgrnself2  29650  nbusgrvtxm1  29669  sizusglecusg  29753  g0wlk0  29940  wlkreslem  29957  lfgrwlkprop  29975  wwlks  30124  wwlksn  30126  wspthsn  30137  iswwlksnon  30142  iswspthsnon  30145  0enwwlksnge1  30153  wwlksnfi  30195  clwwlk  30274  umgrclwwlkge2  30282  clwlkclwwlklem2a4  30288  clwwlkn  30317  clwwlknonmpo  30380  clwwlknon  30381  clwwlk0on0  30383  clwwlknon1le1  30392  1conngr  30485  eupth2lem3lem7  30525  frgr1v  30562  nfrgr2v  30563  1to2vfriswmgr  30570  2wspmdisj  30628  frgrreggt1  30684  frgrreg  30685  frgrregord013  30686  frgrogt3nreg  30688  friendship  30690  avril1  30754  vafval  30895  bafval  30896  smfval  30897  vsfval  30925  bcsiALT  31471  of0r  32964  fracval  33567  fracbas  33568  resvsca  33594  resvlem  33595  cntnevol  34562  signsw0glem  34884  bnj1189  35341  r1wf  35431  noinfepregs  35468  fmlafvel  35775  gonan0  35782  satffun  35799  mvtval  35890  mexval  35892  mexval2  35893  mdvval  35894  mrsubfval  35898  mrsubrn  35903  msubfval  35914  elmsubrn  35918  msubrn  35919  mvhfval  35923  mpstval  35925  msrfval  35927  mstaval  35934  mppsval  35962  mthmval  35965  antnestlaw2  36082  dfrdg3  36184  fvsingle  36308  unisnif  36313  funpartfv  36335  fullfunfv  36337  linedegen  36533  axtcond  36877  csbttc  36908  mh-setindnd  36936  bj-ax6e  37178  axc11n11r  37196  bj-ax12v3ALT  37199  bj-sbsb  37360  bj-nfcsym  37422  bj-snex  37558  bj-restsnid  37616  bj-inftyexpitaudisj  37736  bj-inftyexpidisj  37741  finxpreclem4  37927  finxp00  37935  isinf2  37938  wl-nfs1t  38079  matunitlindflem1  38154  itg2addnclem  38209  ibladdnclem  38214  itgaddnclem1  38216  iblabsnc  38222  iblmulc2nc  38223  ftc1anclem8  38238  ismgmOLD  38388  tsbi1  38671  tsbi2  38672  ac6s6  38710  equid1  39562  ax12fromc15  39568  equid1ALT  39588  dvelimf-o  39592  ax12inda2ALT  39609  ax12inda2  39610  sn-axprlem3  42878  fsuppind  43213  mzpmfp  43369  itgocn  43782  mendbas  43798  mendplusgfval  43799  mendmulrfval  43801  mendsca  43803  mendvscafval  43804  arearect  43833  areaquad  43834  fpwfvss  44029  safesnsupfidom1o  44034  sn1dom  44143  or3or  44640  uneqsn  44642  addcomgi  45055  ax6e2ndeq  45159  2sb5ndVD  45509  2sb5ndALT  45531  sqwvfoura  46833  sqwvfourb  46834  fourierswlem  46835  fouriersw  46836  hspdifhsp  47221  hspmbllem2  47232  hspmbl  47234  et-ltneverrefl  47476  tz6.12-afv  47798  ndmaovcl  47828  tz6.12-afv2  47865  otiunsndisjX  47904  fvmptrab  47917  nltle2tri  47938  fzopredsuc  47949  iccpartiltu  48059  iccpartigtl  48060  iccpartlt  48061  icceuelpartlem  48072  iccpartnel  48075  elsprel  48112  sprssspr  48118  sprsymrelfvlem  48127  prprelprb  48154  prprspr2  48155  fmtnoprmfac1  48205  fmtnoprmfac2  48207  prmdvdsfmtnof1lem2  48225  prminf2  48228  lighneallem4  48250  requad1  48275  requad2  48276  evenprm2  48367  even3prm2  48372  fpprbasnn  48382  stgoldbwt  48429  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  pgnbgreunbgrlem2lem3  48769  upwlkbprop  48791  pgrpgt2nabl  49030  suppmptcfin  49040  linc1  49089  lindslinindsimp2lem5  49126  1aryenef  49309  2aryenef  49320  reorelicc  49374  rrxsphere  49412  fvconst0ci  49553  fvconstdomi  49554  upfval  49838  reldmprcof1  50043  reldmprcof2  50044  lmdfval  50311  cmdfval  50312  setrec2lem1  50355  setrec2mpt  50359