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  1505  norass  1567  ax6e  2412  ax12  2452  exdistrf  2476  equvini  2484  ax12vALT  2498  2ax6e  2500  sb1  2507  sb2  2508  sb4a  2509  dfsb1  2510  dfsb2  2522  sbcom3  2535  sbco2  2540  sbco3  2542  sb9  2548  eujustALT  2597  pm2.61ine  3038  ralcom2  3362  eueq2  3668  moeq3  3670  mo2icl  3672  sbc2or  3748  unineq  4234  csb0  4368  sbcel12  4369  sbcne12  4373  sbcel2  4376  csbidm  4391  csbun  4399  csbin  4400  csbdif  4481  ifsb  4496  ifid  4523  ifnot  4535  ifan  4536  ifor  4537  csbif  4540  elimhyp  4548  elimhyp2v  4549  elimhyp3v  4550  elimhyp4v  4551  elimdhyp  4553  keephyp2v  4555  keephyp3v  4556  rmosn  4680  rabsnif  4684  tppreqb  4768  ssunsn2  4788  n0snor2el  4793  preq12nebg  4823  opthprneg  4825  elpreqprlem  4826  dfopif  4830  csbuni  4898  disjord  5092  sbcbr  5160  unisn2  5269  intabs  5313  class2set  5319  dtruALT2  5335  snexALT  5348  dtruALT  5353  axprlem3  5390  axprlem3OLD  5394  axprglem  5401  axprg  5402  snexOLD  5407  exneq  5411  copsexgwOLD  5467  copsexg  5468  snopeqop  5483  csbopab  5534  dfid3  5553  csbxp  5756  csbcnv  5866  csbres  5975  csbima12  6075  soirri  6120  csbrn  6199  dmsnopss  6210  dmsnsnsn  6216  opswap  6225  unixpid  6282  predres  6337  nsuceq0  6443  ordsssuc2  6451  iotassuni  6508  iotaex  6509  csbiota  6526  dffv3  6874  fvrn0  6906  ndmfv  6910  elfv2ex  6921  fveqres  6922  csbfv12  6923  csbfv  6925  dffv2  6973  fvco4i  6980  fvmptss  6999  fvmptex  7001  fvmptss2  7013  fvmptrabfv  7019  f0cli  7091  fvunsn  7177  fconst5  7205  csbriota  7385  riotassuni  7410  oprabidw  7444  csbov123  7457  csbov  7458  fvmptopab  7468  brfvopab  7470  elimdelov  7509  ovif12  7513  ifmpt2v  7515  ndmovcl  7599  ndmovord  7604  elovmpt3imp  7671  difsnexi  7760  ordsuc  7810  ordsucelsuc  7818  1stval  7988  2ndval  7989  1st2val  8014  2nd2val  8015  el2mpocsbcl  8082  bropopvvv  8087  bropfvvvvlem  8088  bropfvvvv  8089  suppimacnv  8172  suppssdm  8175  ressuppss  8181  suppun  8182  extmptsuppeq  8186  funsssuppss  8188  fczsupp0  8191  suppss  8192  suppss2  8198  suppssfv  8200  suppco  8204  mpoxopynvov0  8216  mpoxopoveqd  8219  pwuninelOLD  8274  smofvon2  8345  om0x  8506  mapssfset  8852  brdomg  8964  snfi  9050  sdomirr  9112  domunsn  9125  2pwuninel  9130  unfi  9165  cnvfi  9170  suppeqfsuppbi  9349  fsuppun  9357  funsnfsupp  9362  fipwuni  9396  oicl  9501  oif  9502  wemapso2  9525  card2on  9526  en2lp  9585  ttrclselem1  9704  tctr  9717  r1tr  9758  rankdmr1  9783  r1pw  9827  r1pwALT  9828  rankuni  9845  scottex  9872  scottexOLD  9873  cardidm  9964  alephcard  10073  alephnbtwn  10074  cfub  10250  cardcf  10253  cflecard  10254  cfle  10255  cflim2  10265  cfidm  10277  isf32lem9  10363  itunisuc  10421  itunitc1  10422  itunitc  10423  ituniiun  10424  axcc2lem  10438  alephreg  10591  pwcfsdom  10592  cfpwsdom  10593  axunndlem1  10604  axpownd  10610  tskmcl  10850  addcompi  10903  addasspi  10904  mulcompi  10905  mulasspi  10906  distrpi  10907  addnidpi  10910  nlt1pi  10915  addcompq  10959  addcomnq  10960  mulcompq  10961  mulcomnq  10962  adderpq  10965  mulerpq  10966  addassnq  10967  mulassnq  10968  distrnq  10970  genpass  11018  addcompr  11030  mulcompr  11032  distrpr  11037  ltexprlem7  11051  addcomsr  11096  addasssr  11097  mulcomsr  11098  mulasssr  11099  distrsr  11100  indval0  12246  uzssz  12908  uzwo  12960  nn01to3  12990  xnn0xaddcl  13287  elixx3g  13411  iooid  13426  elfz2  13568  injresinjlem  13846  injresinj  13847  fleqceilz  13915  modifeq2int  13997  modfzo0difsn  14007  addmodlteq  14010  ltweuz  14025  fzofi  14038  fsuppmapnn0fiubex  14056  hashrabrsn  14436  hashrabsn01  14437  hashrabsn1  14438  elprchashprn2  14460  hashss  14473  hashsn01  14481  hash1snb  14484  hashgt12el  14487  hashgt12el2  14488  hashgt23el  14489  hashfzp1  14496  hashfundm  14507  hash2pwpr  14541  hashge2el2dif  14545  hash3tpde  14558  ffz0iswrd  14606  ccatsymb  14648  swrd00  14712  swrd0  14728  swrdwrdsymb  14732  pfx00  14744  pfx0  14745  repswswrd  14855  0csh0  14864  cshwcl  14869  cshwidxmod  14874  repswcshw  14883  cshw1  14893  s3sndisj  15040  s3iunsndisj  15041  xptrrel  15053  trclfvcotrg  15089  relexpfld  15122  reusq0  15552  modfsummods  15880  dvdsaddre2b  16397  gcdaddmlem  16614  prm23ge5  16907  pcmptcl  16983  prmgaplem5  17147  prmgaplem6  17148  cshwshash  17196  strle1  17250  strfvss  17279  strfvi  17282  setsnid  17300  ressbas  17328  ressbasssg  17329  ressbasssOLD  17332  resseqnbas  17334  ress0  17335  ressress  17339  0rest  17514  firest  17517  topnval  17519  xpsaddlem  17659  xpsvsca  17663  homffval  17778  comfffval  17786  oppchomfval  17802  oppcbas  17806  fullfunc  17997  fthfunc  17998  natfval  18038  fucbas  18052  fuchom  18053  arwval  18132  coafval  18153  xpcbas  18266  xpchomfval  18267  xpccofval  18270  oduval  18376  oduleval  18377  lubfun  18438  glbfun  18451  odujoin  18494  odumeet  18496  ipopos  18624  plusffval  18736  grpidval  18754  gsum0  18786  frmdplusg  18963  frmd0  18969  efmndbas  18980  efmndbasabf  18981  efmndplusg  18989  mgm2nsgrplem2  19031  mgm2nsgrplem3  19032  sgrp2rid2  19038  dfgrp2e  19087  grpinvfval  19102  grpinvfvalALT  19103  grpinvfvi  19106  grpsubfval  19107  grpsubfvalALT  19108  mulgfval  19192  mulgfvalALT  19193  mulgfvi  19196  cntrval  19446  oppgval  19474  oppgplusfval  19475  symgval  19498  snsymgefmndeq  19522  psgnfval  19627  odfval  19659  odfvalALT  19660  oppglsm  19769  efgval  19844  mgpval  20276  mgpplusg  20277  ringidval  20322  opprval  20479  opprmulfval  20480  dvdsrval  20502  invrfval  20530  dvrfval  20543  rrgval  20859  staffval  21007  scaffval  21064  rlmval  21375  rlmsca2  21383  2idlval  21453  nzerooringczr  21693  zrhval  21720  zlmlem  21729  zlmvsca  21734  chrval  21736  evpmss  21799  psgndiflemB  21813  ipffval  21861  thlbas  21909  thlle  21910  thloc  21912  pjfval  21919  dsmmval2  21949  asclfval  22093  psrplusg  22152  psrmulr  22157  psrvscafval  22163  mplval  22203  mplcoe3  22254  evlval  22316  psr1val  22411  vr1val  22417  ply1val  22419  ply1basfvi  22465  ply1plusgfvi  22466  psr1sca2  22475  ply1sca2  22478  ply1ascl  22484  cply1mul  22521  gsummoncoe1  22533  evl1fval  22553  evl1fval1  22556  mamufacex  22618  mavmulsolcl  22773  marrepfval  22782  marepvfval  22787  submafval  22801  mdetfval  22808  mdetfval1  22812  mdetunilem7  22840  mdetunilem8  22841  madufval  22859  minmar1fval  22868  matunitlindflem1  22901  mp2pm2mplem4  23034  toponsspwpw  23147  tgdif0  23217  indislem  23225  resstopn  23411  iocpnfordt  23440  icomnfordt  23441  hmeofval  23984  ussval  24485  nmfval  24814  nghmfval  24948  pcofval  25238  tcphval  25446  ioombl  25793  ibladdlem  26047  itgaddlem1  26050  iblabs  26056  dvbsss  26129  perfdvf  26130  mdegfval  26287  deg1fval  26305  deg1fvi  26310  uc1pval  26365  mon1pval  26367  2irrexpq  26968  lgsqrmodndvds  27589  gausslemma2dlem1a  27601  2lgs  27643  2sqreultblem  27684  2sqreunnltblem  27687  newval  28100  leftval  28114  rightval  28115  lltr  28127  oldssmade  28132  oldss  28135  lrold  28162  ttglem  29332  axcontlem12  29432  vtxval  29457  iedgval  29458  edgval  29506  usgr1v  29716  nbuhgr  29803  nbumgr  29807  uhgrnbgr0nb  29814  nbgr1vtx  29818  nbgrnself2  29820  nbusgrvtxm1  29839  sizusglecusg  29923  g0wlk0  30110  wlkreslem  30127  lfgrwlkprop  30149  wwlks  30303  wwlksn  30305  wspthsn  30316  iswwlksnon  30321  iswspthsnon  30324  0enwwlksnge1  30332  wwlksnfi  30374  clwwlk  30453  umgrclwwlkge2  30461  clwlkclwwlklem2a4  30467  clwwlkn  30496  clwwlknonmpo  30559  clwwlknon  30560  clwwlk0on0  30562  clwwlknon1le1  30571  1conngr  30674  eupth2lem3lem7  30714  frgr1v  30751  nfrgr2v  30752  1to2vfriswmgr  30759  2wspmdisj  30817  frgrreggt1  30873  frgrreg  30874  frgrregord013  30875  frgrogt3nreg  30877  friendship  30879  avril1  30943  vafval  31084  bafval  31085  smfval  31086  vsfval  31114  bcsiALT  31660  of0r  33152  fracval  33745  fracbas  33746  resvsca  33772  resvlem  33773  cntnevol  34739  signsw0glem  35061  bnj1189  35518  r1wf  35603  rankscottu  35636  noinfepregs  35659  kardval  35678  kard0b  35685  kardcard2b  35691  rankkardu  35697  fmlafvel  35964  gonan0  35971  satffun  35988  mvtval  36079  mexval  36081  mexval2  36082  mdvval  36083  mrsubfval  36087  mrsubrn  36092  msubfval  36103  elmsubrn  36107  msubrn  36108  mvhfval  36112  mpstval  36114  msrfval  36116  mstaval  36123  mppsval  36151  mthmval  36154  antnestlaw2  36271  dfrdg3  36373  fvsingle  36497  unisnif  36502  funpartfv  36524  fullfunfv  36526  linedegen  36723  axtcond  37097  csbttc  37128  mh-setindnd  37156  bj-ax6e  37398  axc11n11r  37416  bj-ax12v3ALT  37419  bj-sbsb  37580  bj-nfcsym  37642  bj-snex  37779  bj-restsnid  37837  bj-inftyexpitaudisj  37957  bj-inftyexpidisj  37962  finxpreclem4  38148  finxp00  38156  isinf2  38159  wl-nfs1t  38300  itg2addnclem  38420  ibladdnclem  38425  itgaddnclem1  38427  iblabsnc  38433  iblmulc2nc  38434  ftc1anclem8  38449  ismgmOLD  38600  tsbi1  38881  tsbi2  38882  ac6s6  38920  equid1  39772  ax12fromc15  39778  equid1ALT  39798  dvelimf-o  39802  ax12inda2ALT  39819  ax12inda2  39820  sn-axprlem3  43088  fsuppind  43436  mzpmfp  43592  itgocn  44005  mendbas  44021  mendplusgfval  44022  mendmulrfval  44024  mendsca  44026  mendvscafval  44027  arearect  44056  areaquad  44057  fpwfvss  44252  safesnsupfidom1o  44257  sn1dom  44366  or3or  44863  uneqsn  44865  addcomgi  45278  ax6e2ndeq  45382  2sb5ndVD  45732  2sb5ndALT  45754  sqwvfoura  47056  sqwvfourb  47057  fourierswlem  47058  fouriersw  47059  hspdifhsp  47444  hspmbllem2  47455  hspmbl  47457  et-ltneverrefl  47699  tz6.12-afv  48061  ndmaovcl  48091  tz6.12-afv2  48128  otiunsndisjX  48167  fvmptrab  48180  nltle2tri  48201  fzopredsuc  48212  iccpartiltu  48322  iccpartigtl  48323  iccpartlt  48324  icceuelpartlem  48335  iccpartnel  48338  elsprel  48375  sprssspr  48381  sprsymrelfvlem  48390  prprelprb  48417  prprspr2  48418  fmtnoprmfac1  48468  fmtnoprmfac2  48470  prmdvdsfmtnof1lem2  48488  prminf2  48491  lighneallem4  48513  requad1  48538  requad2  48539  evenprm2  48630  even3prm2  48635  fpprbasnn  48645  stgoldbwt  48692  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  upwlkbprop  49054  pgrpgt2nabl  49296  suppmptcfin  49306  linc1  49355  lindslinindsimp2lem5  49392  1aryenef  49575  2aryenef  49586  reorelicc  49640  rrxsphere  49678  fvconst0ci  49817  fvconstdomi  49818  upfval  50102  reldmprcof1  50307  reldmprcof2  50308  lmdfval  50575  cmdfval  50576  setrec2lem1  50619  setrec2mpt  50623