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  194  pm5.21nii  378  pm5.18  381  biass  384  pm2.61ian  812  ecase3  1033  4cases  1041  pm4.42  1054  ifpid  1077  elimh  1083  3ecase  1477  norass  1539  ax6e  2388  ax12  2428  exdistrf  2452  equvini  2460  ax12vALT  2474  2ax6e  2476  sb1  2483  sb2  2484  sb4a  2485  dfsb1  2486  dfsb2  2498  sbcom3  2511  sbco2  2516  sbco3  2518  sb9  2524  eujustALT  2573  pm2.61ine  3016  ralcom2  3340  eueq2  3657  moeq3  3659  mo2icl  3661  sbc2or  3738  unineq  4229  csb0  4351  sbcel12  4352  sbcne12  4356  sbcel2  4359  csbidm  4374  csbun  4382  csbin  4383  csbdif  4466  ifsb  4481  ifid  4508  ifnot  4520  ifan  4521  ifor  4522  csbif  4525  elimhyp  4533  elimhyp2v  4534  elimhyp3v  4535  elimhyp4v  4536  elimdhyp  4538  keephyp2v  4540  keephyp3v  4541  rmosn  4664  rabsnif  4668  tppreqb  4749  ssunsn2  4771  n0snor2el  4777  preq12nebg  4807  opthprneg  4809  elpreqprlem  4810  dfopif  4814  csbuni  4881  disjord  5075  sbcbr  5141  unisn2  5248  intabs  5287  class2set  5293  dtruALT2  5308  snexALT  5321  dtruALT  5326  axprlem3  5363  axprlem3OLD  5367  axprglem  5374  axprg  5375  snexOLD  5380  exneq  5384  copsexgw  5439  copsexg  5440  snopeqop  5455  csbopab  5504  dfid3  5523  csbxp  5726  csbres  5942  csbima12  6039  soirri  6084  csbrn  6162  dmsnopss  6173  dmsnsnsn  6179  opswap  6188  unixpid  6243  predres  6298  nsuceq0  6403  ordsssuc2  6411  iotassuni  6468  iotaex  6469  csbiota  6486  dffv3  6831  fvrn0  6863  ndmfv  6867  elfv2ex  6878  fveqres  6879  csbfv12  6880  csbfv  6882  dffv2  6930  fvco4i  6936  fvmptss  6955  fvmptex  6957  fvmptss2  6969  fvmptrabfv  6975  f0cli  7045  fvunsn  7128  fconst5  7155  csbriota  7333  riotassuni  7358  oprabidw  7392  csbov123  7405  csbov  7406  fvmptopab  7416  brfvopab  7418  elimdelov  7457  ovif12  7461  ifmpt2v  7463  ndmovcl  7546  ndmovord  7551  elovmpt3imp  7618  difsnexi  7709  ordsuc  7759  ordsucelsuc  7767  1stval  7938  2ndval  7939  1st2val  7964  2nd2val  7965  el2mpocsbcl  8029  bropopvvv  8034  bropfvvvvlem  8035  bropfvvvv  8036  suppimacnv  8118  suppssdm  8121  ressuppss  8127  suppun  8128  extmptsuppeq  8132  funsssuppss  8134  fczsupp0  8137  suppss  8138  suppss2  8144  suppssfv  8146  suppco  8150  mpoxopynvov0  8162  mpoxopoveqd  8165  pwuninel  8219  smofvon2  8290  om0x  8448  mapssfset  8792  brdomg  8899  snfi  8984  sdomirr  9046  domunsn  9059  2pwuninel  9064  unfi  9099  cnvfi  9104  suppeqfsuppbi  9286  fsuppun  9294  funsnfsupp  9299  fipwuni  9333  oicl  9438  oif  9439  wemapso2  9462  card2on  9463  en2lp  9521  ttrclselem1  9640  tctr  9653  r1tr  9694  rankdmr1  9719  r1pw  9763  r1pwALT  9764  rankuni  9781  scottex  9803  cardidm  9877  alephcard  9986  alephnbtwn  9987  cfub  10165  cardcf  10168  cflecard  10169  cfle  10170  cflim2  10179  cfidm  10191  isf32lem9  10277  itunisuc  10335  itunitc1  10336  itunitc  10337  ituniiun  10338  axcc2lem  10352  alephreg  10499  pwcfsdom  10500  cfpwsdom  10501  axunndlem1  10512  axpownd  10518  tskmcl  10758  addcompi  10811  addasspi  10812  mulcompi  10813  mulasspi  10814  distrpi  10815  addnidpi  10818  nlt1pi  10823  addcompq  10867  addcomnq  10868  mulcompq  10869  mulcomnq  10870  adderpq  10873  mulerpq  10874  addassnq  10875  mulassnq  10876  distrnq  10878  genpass  10926  addcompr  10938  mulcompr  10940  distrpr  10945  ltexprlem7  10959  addcomsr  11004  addasssr  11005  mulcomsr  11006  mulasssr  11007  distrsr  11008  indval0  12157  uzssz  12803  uzwo  12855  nn01to3  12885  xnn0xaddcl  13181  elixx3g  13305  iooid  13320  elfz2  13462  injresinjlem  13739  injresinj  13740  fleqceilz  13807  modifeq2int  13889  modfzo0difsn  13899  addmodlteq  13902  ltweuz  13917  fzofi  13930  fsuppmapnn0fiubex  13948  hashrabrsn  14328  hashrabsn01  14329  hashrabsn1  14330  elprchashprn2  14352  hashss  14365  hashsn01  14372  hash1snb  14375  hashgt12el  14378  hashgt12el2  14379  hashgt23el  14380  hashfzp1  14387  hashfundm  14398  hash2pwpr  14432  hashge2el2dif  14436  hash3tpde  14449  ffz0iswrd  14497  ccatsymb  14539  swrd00  14601  swrd0  14615  swrdwrdsymb  14619  pfx00  14631  pfx0  14632  repswswrd  14740  0csh0  14749  cshwcl  14754  cshwidxmod  14759  repswcshw  14768  cshw1  14778  s3sndisj  14923  s3iunsndisj  14924  xptrrel  14936  trclfvcotrg  14972  relexpfld  15005  reusq0  15421  modfsummods  15750  dvdsaddre2b  16270  gcdaddmlem  16487  prm23ge5  16780  pcmptcl  16856  prmgaplem5  17020  prmgaplem6  17021  cshwshash  17069  strle1  17122  strfvss  17151  strfvi  17154  setsnid  17172  ressbas  17200  ressbasssg  17201  ressbasssOLD  17204  resseqnbas  17206  ress0  17207  ressress  17211  0rest  17386  firest  17389  topnval  17391  xpsaddlem  17531  xpsvsca  17535  homffval  17650  comfffval  17658  oppchomfval  17674  oppcbas  17678  fullfunc  17869  fthfunc  17870  natfval  17910  fucbas  17924  fuchom  17925  arwval  18004  coafval  18025  xpcbas  18138  xpchomfval  18139  xpccofval  18142  oduval  18248  oduleval  18249  lubfun  18310  glbfun  18323  odujoin  18366  odumeet  18368  ipopos  18496  plusffval  18608  grpidval  18623  gsum0  18646  frmdplusg  18816  frmd0  18822  efmndbas  18833  efmndbasabf  18834  efmndplusg  18842  mgm2nsgrplem2  18884  mgm2nsgrplem3  18885  sgrp2rid2  18891  dfgrp2e  18933  grpinvfval  18948  grpinvfvalALT  18949  grpinvfvi  18952  grpsubfval  18953  grpsubfvalALT  18954  mulgfval  19039  mulgfvalALT  19040  mulgfvi  19043  cntrval  19288  oppgval  19316  oppgplusfval  19317  symgval  19340  snsymgefmndeq  19364  psgnfval  19469  odfval  19501  odfvalALT  19502  oppglsm  19611  efgval  19686  mgpval  20118  mgpplusg  20119  ringidval  20158  opprval  20312  opprmulfval  20313  dvdsrval  20335  invrfval  20363  dvrfval  20376  rrgval  20668  staffval  20812  scaffval  20869  rlmval  21181  rlmsca2  21189  2idlval  21244  nzerooringczr  21473  zrhval  21500  zlmlem  21509  zlmvsca  21514  chrval  21516  evpmss  21579  psgndiflemB  21593  ipffval  21641  thlbas  21689  thlle  21690  thloc  21692  pjfval  21699  dsmmval2  21729  asclfval  21871  psrplusg  21929  psrmulr  21934  psrvscafval  21940  mplval  21980  mplcoe3  22029  evlval  22091  psr1val  22162  vr1val  22168  ply1val  22170  ply1basfvi  22217  ply1plusgfvi  22218  psr1sca2  22227  ply1sca2  22230  ply1ascl  22236  cply1mul  22274  gsummoncoe1  22286  evl1fval  22306  evl1fval1  22309  mamufacex  22374  mavmulsolcl  22529  marrepfval  22538  marepvfval  22543  submafval  22557  mdetfval  22564  mdetfval1  22568  mdetunilem7  22596  mdetunilem8  22597  madufval  22615  minmar1fval  22624  mp2pm2mplem4  22787  toponsspwpw  22900  tgdif0  22970  indislem  22978  resstopn  23164  iocpnfordt  23193  icomnfordt  23194  hmeofval  23736  ussval  24237  nmfval  24566  nghmfval  24700  pcofval  24990  tcphval  25198  ioombl  25545  ibladdlem  25800  itgaddlem1  25803  iblabs  25809  dvbsss  25882  perfdvf  25883  mdegfval  26040  deg1fval  26058  deg1fvi  26063  uc1pval  26118  mon1pval  26120  2irrexpq  26711  lgsqrmodndvds  27333  gausslemma2dlem1a  27345  2lgs  27387  2sqreultblem  27428  2sqreunnltblem  27431  newval  27844  leftval  27858  rightval  27859  lltr  27871  oldssmade  27876  oldss  27879  lrold  27906  ttglem  28961  axcontlem12  29061  vtxval  29086  iedgval  29087  edgval  29135  usgr1v  29342  nbuhgr  29429  nbumgr  29433  uhgrnbgr0nb  29440  nbgr1vtx  29444  nbgrnself2  29446  nbusgrvtxm1  29465  sizusglecusg  29550  g0wlk0  29737  wlkreslem  29754  lfgrwlkprop  29772  wwlks  29921  wwlksn  29923  wspthsn  29934  iswwlksnon  29939  iswspthsnon  29942  0enwwlksnge1  29950  wwlksnfi  29992  clwwlk  30071  umgrclwwlkge2  30079  clwlkclwwlklem2a4  30085  clwwlkn  30114  clwwlknonmpo  30177  clwwlknon  30178  clwwlk0on0  30180  clwwlknon1le1  30189  1conngr  30282  eupth2lem3lem7  30322  frgr1v  30359  nfrgr2v  30360  1to2vfriswmgr  30367  2wspmdisj  30425  frgrreggt1  30481  frgrreg  30482  frgrregord013  30483  frgrogt3nreg  30485  friendship  30487  avril1  30551  vafval  30692  bafval  30693  smfval  30694  vsfval  30722  bcsiALT  31268  of0r  32770  fracval  33383  fracbas  33384  resvsca  33410  resvlem  33411  cntnevol  34391  signsw0glem  34716  bnj1189  35170  r1wf  35258  noinfepregs  35296  fmlafvel  35586  gonan0  35593  satffun  35610  mvtval  35701  mexval  35703  mexval2  35704  mdvval  35705  mrsubfval  35709  mrsubrn  35714  msubfval  35725  elmsubrn  35729  msubrn  35730  mvhfval  35734  mpstval  35736  msrfval  35738  mstaval  35745  mppsval  35773  mthmval  35776  antnestlaw2  35893  dfrdg3  35995  fvsingle  36119  unisnif  36124  funpartfv  36146  fullfunfv  36148  linedegen  36344  axtcond  36679  csbttc  36710  mh-setindnd  36738  bj-ax6e  36981  axc11n11r  36999  bj-ax12v3ALT  37002  bj-sbsb  37163  bj-nfcsym  37225  bj-snex  37361  bj-restsnid  37418  bj-inftyexpitaudisj  37538  bj-inftyexpidisj  37543  finxpreclem4  37727  finxp00  37735  isinf2  37738  wl-nfs1t  37879  matunitlindflem1  37954  itg2addnclem  38009  ibladdnclem  38014  itgaddnclem1  38016  iblabsnc  38022  iblmulc2nc  38023  ftc1anclem8  38038  ismgmOLD  38188  tsbi1  38471  tsbi2  38472  ac6s6  38510  equid1  39362  ax12fromc15  39368  equid1ALT  39388  dvelimf-o  39392  ax12inda2ALT  39409  ax12inda2  39410  sn-axprlem3  42676  fsuppind  43040  mzpmfp  43196  itgocn  43613  mendbas  43629  mendplusgfval  43630  mendmulrfval  43632  mendsca  43634  mendvscafval  43635  arearect  43664  areaquad  43665  fpwfvss  43860  safesnsupfidom1o  43865  sn1dom  43974  or3or  44471  uneqsn  44473  addcomgi  44903  ax6e2ndeq  45007  2sb5ndVD  45357  2sb5ndALT  45379  sqwvfoura  46677  sqwvfourb  46678  fourierswlem  46679  fouriersw  46680  hspdifhsp  47065  hspmbllem2  47076  hspmbl  47078  et-ltneverrefl  47320  tz6.12-afv  47636  ndmaovcl  47666  tz6.12-afv2  47703  otiunsndisjX  47742  fvmptrab  47755  nltle2tri  47776  fzopredsuc  47787  iccpartiltu  47897  iccpartigtl  47898  iccpartlt  47899  icceuelpartlem  47910  iccpartnel  47913  elsprel  47950  sprssspr  47956  sprsymrelfvlem  47965  prprelprb  47992  prprspr2  47993  fmtnoprmfac1  48043  fmtnoprmfac2  48045  prmdvdsfmtnof1lem2  48063  prminf2  48066  lighneallem4  48088  requad1  48113  requad2  48114  evenprm2  48205  even3prm2  48210  fpprbasnn  48220  stgoldbwt  48267  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  upwlkbprop  48629  pgrpgt2nabl  48857  suppmptcfin  48867  linc1  48916  lindslinindsimp2lem5  48953  1aryenef  49136  2aryenef  49147  reorelicc  49201  rrxsphere  49239  fvconst0ci  49381  fvconstdomi  49382  upfval  49666  reldmprcof1  49871  reldmprcof2  49872  lmdfval  50139  cmdfval  50140  setrec2lem1  50183  setrec2mpt  50187