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  808  ecase3  1028  4cases  1037  pm4.42  1050  ifpid  1074  elimh  1081  3ecase  1472  norass  1535  ax6e  2383  ax12  2423  exdistrf  2447  equvini  2455  ax12vALT  2469  2ax6e  2471  sb1  2479  sb2  2480  sb1OLD  2482  sb4a  2484  dfsb1  2485  dfsb2  2497  sbcom3  2510  sbco2  2515  sbco3  2517  sb9  2523  nfsbOLD  2528  eujustALT  2572  pm2.61ine  3027  ralcom2  3288  eueq2  3640  moeq3  3642  mo2icl  3644  sbc2or  3720  unineq  4208  csb0  4338  sbcel12  4339  sbcne12  4343  sbcel2  4346  csbidm  4361  csbun  4369  csbin  4370  ralidmOLD  4443  csbdif  4455  ifsb  4469  ifid  4496  ifnot  4508  ifan  4509  ifor  4510  csbif  4513  elimhyp  4521  elimhyp2v  4522  elimhyp3v  4523  elimhyp4v  4524  elimdhyp  4526  keephyp2v  4528  keephyp3v  4529  rmosn  4652  rabsnif  4656  tppreqb  4735  ssunsn2  4757  n0snor2el  4761  preq12nebg  4790  opthprneg  4792  elpreqprlem  4793  dfopifOLD  4798  csbuni  4867  disjord  5058  sbcbr  5125  unisn2  5231  intabs  5261  class2set  5271  dtru  5288  snexALT  5301  dtruALT  5306  axprlem3  5343  snex  5349  dtruALT2  5353  copsexgw  5398  copsexg  5399  snopeqop  5414  csbopab  5461  0nelopabOLD  5472  dfid3  5483  csbxp  5676  csbres  5883  csbima12  5976  soirri  6020  csbrn  6095  dmsnopss  6106  dmsnsnsn  6112  opswap  6121  unixpid  6176  nsuceq0  6331  ordsssuc2  6339  iotassuni  6397  iotaex  6398  csbiota  6411  dffv3  6752  fvrn0  6784  ndmfv  6786  elfv2ex  6797  fveqres  6798  csbfv12  6799  csbfv  6801  dffv2  6845  fvco4i  6851  fvmptss  6869  fvmptex  6871  fvmptss2  6882  fvmptrabfv  6888  f0cli  6956  fvunsn  7033  fconst5  7063  csbriota  7228  riotassuni  7253  oprabidw  7286  csbov123  7297  csbov  7298  fvmptopab  7308  brfvopab  7310  elimdelov  7349  ovif12  7352  ndmovcl  7435  ndmovord  7440  elovmpt3imp  7504  difsnexi  7589  ordsuc  7636  ordsucelsuc  7644  1stval  7806  2ndval  7807  1st2val  7832  2nd2val  7833  el2mpocsbcl  7896  bropopvvv  7901  bropfvvvvlem  7902  bropfvvvv  7903  suppimacnv  7961  suppssdm  7964  ressuppss  7970  suppun  7971  extmptsuppeq  7975  funsssuppss  7977  fczsupp0  7980  suppss  7981  suppssOLD  7982  suppssov1  7985  suppss2  7987  suppssfv  7989  suppco  7993  mpoxopynvov0  8005  mpoxopoveqd  8008  pwuninel  8062  smofvon2  8158  om0x  8311  mapssfset  8597  brdomg  8703  snfi  8788  sdomirr  8850  domunsn  8863  2pwuninel  8868  snnen2o  8903  unfi  8917  cnvfi  8924  suppeqfsuppbi  9072  fsuppun  9077  funsnfsupp  9082  fipwuni  9115  oicl  9218  oif  9219  wemapso2  9242  card2on  9243  en2lp  9294  trpredlem1  9405  tctr  9429  r1tr  9465  rankdmr1  9490  r1pw  9534  r1pwALT  9535  rankuni  9552  scottex  9574  cardidm  9648  alephcard  9757  alephnbtwn  9758  cfub  9936  cardcf  9939  cflecard  9940  cfle  9941  cflim2  9950  cfidm  9962  isf32lem9  10048  itunisuc  10106  itunitc1  10107  itunitc  10108  ituniiun  10109  axcc2lem  10123  alephreg  10269  pwcfsdom  10270  cfpwsdom  10271  axunndlem1  10282  axpownd  10288  tskmcl  10528  addcompi  10581  addasspi  10582  mulcompi  10583  mulasspi  10584  distrpi  10585  addnidpi  10588  nlt1pi  10593  addcompq  10637  addcomnq  10638  mulcompq  10639  mulcomnq  10640  adderpq  10643  mulerpq  10644  addassnq  10645  mulassnq  10646  distrnq  10648  genpass  10696  addcompr  10708  mulcompr  10710  distrpr  10715  ltexprlem7  10729  addcomsr  10774  addasssr  10775  mulcomsr  10776  mulasssr  10777  distrsr  10778  uzssz  12532  uzwo  12580  nn01to3  12610  xnn0xaddcl  12898  elixx3g  13021  iooid  13036  elfz2  13175  injresinjlem  13435  injresinj  13436  fleqceilz  13502  modifeq2int  13581  modfzo0difsn  13591  addmodlteq  13594  ltweuz  13609  fzofi  13622  fsuppmapnn0fiubex  13640  hashrabrsn  14015  hashrabsn01  14016  hashrabsn1  14017  elprchashprn2  14039  hashss  14052  hashsn01  14059  hash1snb  14062  hashgt12el  14065  hashgt12el2  14066  hashgt23el  14067  hashfzp1  14074  hash2pwpr  14118  hashge2el2dif  14122  ffz0iswrd  14172  ccatsymb  14215  swrd00  14285  swrd0  14299  swrdwrdsymb  14303  pfx00  14315  pfx0  14316  repswswrd  14425  0csh0  14434  cshwcl  14439  cshwidxmod  14444  repswcshw  14453  cshw1  14463  s3sndisj  14606  s3iunsndisj  14607  xptrrel  14619  trclfvcotrg  14655  relexpfld  14688  reusq0  15102  modfsummods  15433  dvdsaddre2b  15944  gcdaddmlem  16159  prm23ge5  16444  pcmptcl  16520  prmgaplem5  16684  prmgaplem6  16685  cshwshash  16734  strle1  16787  strfvss  16816  strfvi  16819  setsnid  16838  setsnidOLD  16839  ressbas  16873  ressbasOLD  16874  ressbasss  16876  resseqnbas  16877  resslemOLD  16878  ress0  16879  ressress  16884  0rest  17057  firest  17060  topnval  17062  xpsaddlem  17201  xpsvsca  17205  homffval  17316  comfffval  17324  oppchomfval  17340  oppchomfvalOLD  17341  oppcbas  17345  oppcbasOLD  17346  fullfunc  17538  fthfunc  17539  natfval  17578  fucbas  17593  fuchom  17594  fuchomOLD  17595  arwval  17674  coafval  17695  xpcbas  17811  xpchomfval  17812  xpccofval  17815  oduval  17922  oduleval  17923  lubfun  17985  glbfun  17998  odujoin  18041  odumeet  18043  ipopos  18169  plusffval  18247  grpidval  18260  gsum0  18283  frmdplusg  18408  frmd0  18414  efmndbas  18425  efmndbasabf  18426  efmndplusg  18434  mgm2nsgrplem2  18473  mgm2nsgrplem3  18474  sgrp2rid2  18480  dfgrp2e  18520  grpinvfval  18533  grpinvfvalALT  18534  grpinvfvi  18537  grpsubfval  18538  grpsubfvalALT  18539  mulgfval  18617  mulgfvalALT  18618  mulgfvi  18621  cntrval  18840  oppgval  18866  oppgplusfval  18867  symgval  18891  snsymgefmndeq  18917  psgnfval  19023  odfval  19055  odfvalALT  19056  oppglsm  19162  efgval  19238  mgpval  19638  mgpplusg  19639  ringidval  19654  opprval  19778  opprmulfval  19779  dvdsrval  19802  invrfval  19830  dvrfval  19841  staffval  20022  scaffval  20056  rlmval  20374  rlmsca2  20384  2idlval  20417  rrgval  20471  zrhval  20621  zlmlem  20630  zlmlemOLD  20631  zlmvsca  20639  chrval  20641  evpmss  20703  psgndiflemB  20717  ipffval  20765  thlbas  20813  thlle  20814  thloc  20816  pjfval  20823  dsmmval2  20853  asclfval  20993  psrplusg  21060  psrmulr  21063  psrvscafval  21069  mplval  21107  mplcoe3  21149  evlval  21215  psr1val  21267  vr1val  21273  ply1val  21275  ply1basfvi  21322  ply1plusgfvi  21323  psr1sca2  21332  ply1sca2  21335  ply1ascl  21339  cply1mul  21375  gsummoncoe1  21385  evl1fval  21404  evl1fval1  21407  mamufacex  21448  mavmulsolcl  21608  marrepfval  21617  marepvfval  21622  submafval  21636  mdetfval  21643  mdetfval1  21647  mdetunilem7  21675  mdetunilem8  21676  madufval  21694  minmar1fval  21703  mp2pm2mplem4  21866  toponsspwpw  21979  tgdif0  22050  indislem  22058  resstopn  22245  iocpnfordt  22274  icomnfordt  22275  hmeofval  22817  ussval  23319  nmfval  23650  nghmfval  23792  pcofval  24079  tcphval  24287  ioombl  24634  ibladdlem  24889  itgaddlem1  24892  iblabs  24898  dvbsss  24971  perfdvf  24972  mdegfval  25132  deg1fval  25150  deg1fvi  25155  uc1pval  25209  mon1pval  25211  2irrexpq  25790  lgsqrmodndvds  26406  gausslemma2dlem1a  26418  2lgs  26460  2sqreultblem  26501  2sqreunnltblem  26504  ttglem  27141  ttglemOLD  27142  axcontlem12  27246  vtxval  27273  iedgval  27274  edgval  27322  usgr1v  27526  nbuhgr  27613  nbumgr  27617  uhgrnbgr0nb  27624  nbgr1vtx  27628  nbgrnself2  27630  nbusgrvtxm1  27649  sizusglecusg  27733  g0wlk0  27921  wlkreslem  27939  lfgrwlkprop  27957  wwlks  28101  wwlksn  28103  wspthsn  28114  iswwlksnon  28119  iswspthsnon  28122  0enwwlksnge1  28130  wwlksnfi  28172  clwwlk  28248  umgrclwwlkge2  28256  clwlkclwwlklem2a4  28262  clwwlkn  28291  clwwlknonmpo  28354  clwwlknon  28355  clwwlk0on0  28357  clwwlknon1le1  28366  1conngr  28459  eupth2lem3lem7  28499  frgr1v  28536  nfrgr2v  28537  1to2vfriswmgr  28544  2wspmdisj  28602  frgrreggt1  28658  frgrreg  28659  frgrregord013  28660  frgrogt3nreg  28662  friendship  28664  avril1  28728  vafval  28866  bafval  28867  smfval  28868  vsfval  28896  bcsiALT  29442  resvsca  31431  resvlem  31432  resvlemOLD  31433  cntnevol  32096  signsw0glem  32432  bnj1189  32889  hashfundm  32974  fmlafvel  33247  gonan0  33254  satffun  33271  mvtval  33362  mexval  33364  mexval2  33365  mdvval  33366  mrsubfval  33370  mrsubrn  33375  msubfval  33386  elmsubrn  33390  msubrn  33391  mvhfval  33395  mpstval  33397  msrfval  33399  mstaval  33406  mppsval  33434  mthmval  33437  dfrdg3  33678  ttrclselem1  33711  newval  33966  leftval  33974  rightval  33975  oldssmade  33987  lrold  34004  fvsingle  34149  unisnif  34154  funpartfv  34174  fullfunfv  34176  linedegen  34372  bj-ax6e  34776  axc11n11r  34792  bj-ax12v3ALT  34795  bj-dtru  34926  bj-sbsb  34947  bj-nfcsym  35011  bj-restsnid  35185  bj-inftyexpitaudisj  35303  bj-inftyexpidisj  35308  finxpreclem4  35492  finxp00  35500  isinf2  35503  wl-nfs1t  35623  matunitlindflem1  35700  itg2addnclem  35755  ibladdnclem  35760  itgaddnclem1  35762  iblabsnc  35768  iblmulc2nc  35769  ftc1anclem8  35784  ismgmOLD  35935  tsbi1  36218  tsbi2  36219  ac6s6  36257  equid1  36840  ax12fromc15  36846  equid1ALT  36866  dvelimf-o  36870  ax12inda2ALT  36887  ax12inda2  36888  sn-axprlem3  40114  sn-dtru  40116  sn-iotassuni  40122  sn-iotaex  40123  fsuppind  40202  mzpmfp  40485  itgocn  40905  mendbas  40925  mendplusgfval  40926  mendmulrfval  40928  mendsca  40930  mendvscafval  40931  arearect  40962  areaquad  40963  sn1dom  41031  or3or  41520  uneqsn  41522  addcomgi  41963  ax6e2ndeq  42068  2sb5ndVD  42419  2sb5ndALT  42441  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  hspdifhsp  44044  hspmbllem2  44055  hspmbl  44057  tz6.12-afv  44552  ndmaovcl  44582  tz6.12-afv2  44619  otiunsndisjX  44658  fvmptrab  44671  nltle2tri  44693  fzopredsuc  44703  iccpartiltu  44762  iccpartigtl  44763  iccpartlt  44764  icceuelpartlem  44775  iccpartnel  44778  elsprel  44815  sprssspr  44821  sprsymrelfvlem  44830  prprelprb  44857  prprspr2  44858  fmtnoprmfac1  44905  fmtnoprmfac2  44907  prmdvdsfmtnof1lem2  44925  prminf2  44928  lighneallem4  44950  requad1  44962  requad2  44963  evenprm2  45054  even3prm2  45059  fpprbasnn  45069  stgoldbwt  45116  upwlkbprop  45188  nzerooringczr  45518  pgrpgt2nabl  45590  suppmptcfin  45603  linc1  45654  lindslinindsimp2lem5  45691  1aryenef  45879  2aryenef  45890  reorelicc  45944  rrxsphere  45982  fvconst0ci  46074  fvconstdomi  46075  setrec2lem1  46285