Theorem pm2.61i 185

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 161	. 2 ⊢ (¬ 𝜓 → 𝜓)
4	3	pm2.18i 131	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  186  pm2.61nii  187  pm2.61iii  188  pm2.65i  197  pm5.21nii  383  pm5.18  386  biass  389  pm2.61ian  812  ecase3  1032  4cases  1041  pm4.42  1054  ifpid  1078  elimh  1085  3ecase  1476  norass  1539  ax6e  2382  ax12  2422  exdistrf  2446  equvini  2454  ax12vALT  2468  2ax6e  2470  sb1  2478  sb2  2479  sb1OLD  2481  sb4a  2483  dfsb1  2484  dfsb2  2496  sbcom3  2509  sbco2  2514  sbco3  2516  sb9  2522  nfsbOLD  2527  eujustALT  2571  pm2.61ine  3025  ralcom2  3275  eueq2  3623  moeq3  3625  mo2icl  3627  sbc2or  3703  unineq  4192  csb0  4322  sbcel12  4323  sbcne12  4327  sbcel2  4330  csbidm  4345  csbun  4353  csbin  4354  ralidmOLD  4427  ifsb  4452  ifid  4479  ifnot  4491  ifan  4492  ifor  4493  csbif  4496  elimhyp  4504  elimhyp2v  4505  elimhyp3v  4506  elimhyp4v  4507  elimdhyp  4509  keephyp2v  4511  keephyp3v  4512  rmosn  4635  rabsnif  4639  tppreqb  4718  ssunsn2  4740  n0snor2el  4744  preq12nebg  4773  opthprneg  4775  elpreqprlem  4776  dfopifOLD  4781  csbuni  4850  disjord  5041  sbcbr  5108  unisn2  5205  intabs  5235  class2set  5245  dtru  5263  snexALT  5276  dtruALT  5281  axprlem3  5318  snex  5324  dtruALT2  5328  copsexgw  5373  copsexg  5374  snopeqop  5389  csbopab  5436  0nelopabOLD  5447  dfid3  5457  csbxp  5647  csbres  5854  csbima12  5947  soirri  5991  csbrn  6066  dmsnopss  6077  dmsnsnsn  6083  opswap  6092  unixpid  6147  nsuceq0  6293  ordsssuc2  6301  iotassuni  6359  iotaex  6360  csbiota  6373  dffv3  6713  fvrn0  6745  ndmfv  6747  elfv2ex  6758  fveqres  6759  csbfv12  6760  csbfv  6762  dffv2  6806  fvco4i  6812  fvmptss  6830  fvmptex  6832  fvmptss2  6843  fvmptrabfv  6849  f0cli  6917  fvunsn  6994  fconst5  7021  csbriota  7186  riotassuni  7211  oprabidw  7244  csbov123  7255  csbov  7256  fvmptopab  7266  brfvopab  7268  elimdelov  7307  ovif12  7310  ndmovcl  7393  ndmovord  7398  elovmpt3imp  7462  difsnexi  7546  ordsuc  7593  ordsucelsuc  7601  1stval  7763  2ndval  7764  1st2val  7789  2nd2val  7790  el2mpocsbcl  7853  bropopvvv  7858  bropfvvvvlem  7859  bropfvvvv  7860  suppimacnv  7916  suppssdm  7919  ressuppss  7925  suppun  7926  extmptsuppeq  7930  funsssuppss  7932  fczsupp0  7935  suppss  7936  suppssOLD  7937  suppssov1  7940  suppss2  7942  suppssfv  7944  suppco  7948  mpoxopynvov0  7960  mpoxopoveqd  7963  pwuninel  8017  smofvon2  8093  om0x  8246  mapssfset  8532  brdomg  8638  snfi  8721  sdomirr  8783  domunsn  8796  2pwuninel  8801  snnen2o  8836  unfi  8850  cnvfi  8857  suppeqfsuppbi  8999  fsuppun  9004  funsnfsupp  9009  fipwuni  9042  oicl  9145  oif  9146  wemapso2  9169  card2on  9170  en2lp  9221  trpredlem1  9332  tctr  9356  r1tr  9392  rankdmr1  9417  r1pw  9461  r1pwALT  9462  rankuni  9479  scottex  9501  cardidm  9575  alephcard  9684  alephnbtwn  9685  cfub  9863  cardcf  9866  cflecard  9867  cfle  9868  cflim2  9877  cfidm  9889  isf32lem9  9975  itunisuc  10033  itunitc1  10034  itunitc  10035  ituniiun  10036  axcc2lem  10050  alephreg  10196  pwcfsdom  10197  cfpwsdom  10198  axunndlem1  10209  axpownd  10215  tskmcl  10455  addcompi  10508  addasspi  10509  mulcompi  10510  mulasspi  10511  distrpi  10512  addnidpi  10515  nlt1pi  10520  addcompq  10564  addcomnq  10565  mulcompq  10566  mulcomnq  10567  adderpq  10570  mulerpq  10571  addassnq  10572  mulassnq  10573  distrnq  10575  genpass  10623  addcompr  10635  mulcompr  10637  distrpr  10642  ltexprlem7  10656  addcomsr  10701  addasssr  10702  mulcomsr  10703  mulasssr  10704  distrsr  10705  uzssz  12459  uzwo  12507  nn01to3  12537  xnn0xaddcl  12825  elixx3g  12948  iooid  12963  elfz2  13102  injresinjlem  13362  injresinj  13363  fleqceilz  13427  modifeq2int  13506  modfzo0difsn  13516  addmodlteq  13519  ltweuz  13534  fzofi  13547  fsuppmapnn0fiubex  13565  hashrabrsn  13939  hashrabsn01  13940  hashrabsn1  13941  elprchashprn2  13963  hashss  13976  hashsn01  13983  hash1snb  13986  hashgt12el  13989  hashgt12el2  13990  hashgt23el  13991  hashfzp1  13998  hash2pwpr  14042  hashge2el2dif  14046  ffz0iswrd  14096  ccatsymb  14139  swrd00  14209  swrd0  14223  swrdwrdsymb  14227  pfx00  14239  pfx0  14240  repswswrd  14349  0csh0  14358  cshwcl  14363  cshwidxmod  14368  repswcshw  14377  cshw1  14387  s3sndisj  14530  s3iunsndisj  14531  xptrrel  14543  trclfvcotrg  14579  relexpfld  14612  reusq0  15026  modfsummods  15357  dvdsaddre2b  15868  gcdaddmlem  16083  prm23ge5  16368  pcmptcl  16444  prmgaplem5  16608  prmgaplem6  16609  cshwshash  16658  strle1  16711  strfvss  16740  strfvi  16743  setsnid  16759  ressbas  16790  ressbasss  16792  resseqnbas  16793  resslemOLD  16794  ress0  16795  ressress  16799  0rest  16934  firest  16937  topnval  16939  xpsaddlem  17078  xpsvsca  17082  homffval  17193  comfffval  17201  oppchomfval  17217  oppchomfvalOLD  17218  oppcbas  17222  fullfunc  17413  fthfunc  17414  natfval  17453  fucbas  17468  fuchom  17469  fuchomOLD  17470  arwval  17549  coafval  17570  xpcbas  17685  xpchomfval  17686  xpccofval  17689  oduval  17796  oduleval  17797  lubfun  17858  glbfun  17871  odujoin  17914  odumeet  17916  ipopos  18042  plusffval  18120  grpidval  18133  gsum0  18156  frmdplusg  18281  frmd0  18287  efmndbas  18298  efmndbasabf  18299  efmndplusg  18307  mgm2nsgrplem2  18346  mgm2nsgrplem3  18347  sgrp2rid2  18353  dfgrp2e  18393  grpinvfval  18406  grpinvfvalALT  18407  grpinvfvi  18410  grpsubfval  18411  grpsubfvalALT  18412  mulgfval  18490  mulgfvalALT  18491  mulgfvi  18494  cntrval  18713  oppgval  18739  oppgplusfval  18740  symgval  18761  snsymgefmndeq  18787  psgnfval  18892  odfval  18924  odfvalALT  18925  oppglsm  19031  efgval  19107  mgpval  19507  mgpplusg  19508  ringidval  19518  opprval  19642  opprmulfval  19643  dvdsrval  19663  invrfval  19691  dvrfval  19702  staffval  19883  scaffval  19917  rlmval  20228  rlmsca2  20238  2idlval  20271  rrgval  20325  zrhval  20474  zlmlem  20483  zlmvsca  20488  chrval  20490  evpmss  20548  psgndiflemB  20562  ipffval  20610  thlbas  20658  thlle  20659  thloc  20661  pjfval  20668  dsmmval2  20698  asclfval  20838  psrplusg  20906  psrmulr  20909  psrvscafval  20915  mplval  20953  mplcoe3  20995  evlval  21055  psr1val  21107  vr1val  21113  ply1val  21115  ply1basfvi  21162  ply1plusgfvi  21163  psr1sca2  21172  ply1sca2  21175  ply1ascl  21179  cply1mul  21215  gsummoncoe1  21225  evl1fval  21244  evl1fval1  21247  mamufacex  21288  mavmulsolcl  21448  marrepfval  21457  marepvfval  21462  submafval  21476  mdetfval  21483  mdetfval1  21487  mdetunilem7  21515  mdetunilem8  21516  madufval  21534  minmar1fval  21543  mp2pm2mplem4  21706  toponsspwpw  21819  tgdif0  21889  indislem  21897  resstopn  22083  iocpnfordt  22112  icomnfordt  22113  hmeofval  22655  ussval  23157  nmfval  23486  nghmfval  23620  pcofval  23907  tcphval  24115  ioombl  24462  ibladdlem  24717  itgaddlem1  24720  iblabs  24726  dvbsss  24799  perfdvf  24800  mdegfval  24960  deg1fval  24978  deg1fvi  24983  uc1pval  25037  mon1pval  25039  2irrexpq  25618  lgsqrmodndvds  26234  gausslemma2dlem1a  26246  2lgs  26288  2sqreultblem  26329  2sqreunnltblem  26332  ttglem  26967  axcontlem12  27066  vtxval  27091  iedgval  27092  edgval  27140  usgr1v  27344  nbuhgr  27431  nbumgr  27435  uhgrnbgr0nb  27442  nbgr1vtx  27446  nbgrnself2  27448  nbusgrvtxm1  27467  sizusglecusg  27551  g0wlk0  27739  wlkreslem  27757  lfgrwlkprop  27775  wwlks  27919  wwlksn  27921  wspthsn  27932  iswwlksnon  27937  iswspthsnon  27940  0enwwlksnge1  27948  wwlksnfi  27990  clwwlk  28066  umgrclwwlkge2  28074  clwlkclwwlklem2a4  28080  clwwlkn  28109  clwwlknonmpo  28172  clwwlknon  28173  clwwlk0on0  28175  clwwlknon1le1  28184  1conngr  28277  eupth2lem3lem7  28317  frgr1v  28354  nfrgr2v  28355  1to2vfriswmgr  28362  2wspmdisj  28420  frgrreggt1  28476  frgrreg  28477  frgrregord013  28478  frgrogt3nreg  28480  friendship  28482  avril1  28546  vafval  28684  bafval  28685  smfval  28686  vsfval  28714  bcsiALT  29260  resvsca  31248  resvlem  31249  cntnevol  31908  signsw0glem  32244  bnj1189  32702  hashfundm  32787  fmlafvel  33060  gonan0  33067  satffun  33084  mvtval  33175  mexval  33177  mexval2  33178  mdvval  33179  mrsubfval  33183  mrsubrn  33188  msubfval  33199  elmsubrn  33203  msubrn  33204  mvhfval  33208  mpstval  33210  msrfval  33212  mstaval  33219  mppsval  33247  mthmval  33250  dfrdg3  33491  newval  33776  leftval  33784  rightval  33785  oldssmade  33797  lrold  33814  fvsingle  33959  unisnif  33964  funpartfv  33984  fullfunfv  33986  linedegen  34182  bj-ax6e  34586  axc11n11r  34602  bj-ax12v3ALT  34605  bj-dtru  34736  bj-sbsb  34757  bj-nfcsym  34821  bj-restsnid  34993  bj-inftyexpitaudisj  35111  bj-inftyexpidisj  35116  csbdif  35233  finxpreclem4  35302  finxp00  35310  isinf2  35313  wl-nfs1t  35433  matunitlindflem1  35510  itg2addnclem  35565  ibladdnclem  35570  itgaddnclem1  35572  iblabsnc  35578  iblmulc2nc  35579  ftc1anclem8  35594  ismgmOLD  35745  tsbi1  36028  tsbi2  36029  ac6s6  36067  equid1  36650  ax12fromc15  36656  equid1ALT  36676  dvelimf-o  36680  ax12inda2ALT  36697  ax12inda2  36698  sn-axprlem3  39908  sn-dtru  39910  fsuppind  39989  mzpmfp  40272  itgocn  40692  mendbas  40712  mendplusgfval  40713  mendmulrfval  40715  mendsca  40717  mendvscafval  40718  arearect  40749  areaquad  40750  sn1dom  40818  or3or  41308  uneqsn  41310  addcomgi  41747  ax6e2ndeq  41852  2sb5ndVD  42203  2sb5ndALT  42225  sqwvfoura  43444  sqwvfourb  43445  fourierswlem  43446  fouriersw  43447  hspdifhsp  43829  hspmbllem2  43840  hspmbl  43842  tz6.12-afv  44337  ndmaovcl  44367  tz6.12-afv2  44404  otiunsndisjX  44443  fvmptrab  44456  nltle2tri  44478  fzopredsuc  44488  iccpartiltu  44547  iccpartigtl  44548  iccpartlt  44549  icceuelpartlem  44560  iccpartnel  44563  elsprel  44600  sprssspr  44606  sprsymrelfvlem  44615  prprelprb  44642  prprspr2  44643  fmtnoprmfac1  44690  fmtnoprmfac2  44692  prmdvdsfmtnof1lem2  44710  prminf2  44713  lighneallem4  44735  requad1  44747  requad2  44748  evenprm2  44839  even3prm2  44844  fpprbasnn  44854  stgoldbwt  44901  upwlkbprop  44973  nzerooringczr  45303  pgrpgt2nabl  45375  suppmptcfin  45388  linc1  45439  lindslinindsimp2lem5  45476  1aryenef  45664  2aryenef  45675  reorelicc  45729  rrxsphere  45767  fvconst0ci  45859  fvconstdomi  45860  setrec2lem1  46070