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  810  ecase3  1030  4cases  1039  pm4.42  1052  ifpid  1076  elimh  1083  3ecase  1474  norass  1538  ax6e  2381  ax12  2421  exdistrf  2445  equvini  2453  ax12vALT  2467  2ax6e  2469  sb1  2476  sb2  2477  sb4a  2478  dfsb1  2479  dfsb2  2491  sbcom3  2504  sbco2  2509  sbco3  2511  sb9  2517  eujustALT  2565  pm2.61ine  3024  ralcom2  3348  eueq2  3671  moeq3  3673  mo2icl  3675  sbc2or  3751  unineq  4242  csb0  4372  sbcel12  4373  sbcne12  4377  sbcel2  4380  csbidm  4395  csbun  4403  csbin  4404  ralidmOLD  4478  csbdif  4490  ifsb  4504  ifid  4531  ifnot  4543  ifan  4544  ifor  4545  csbif  4548  elimhyp  4556  elimhyp2v  4557  elimhyp3v  4558  elimhyp4v  4559  elimdhyp  4561  keephyp2v  4563  keephyp3v  4564  rmosn  4685  rabsnif  4689  tppreqb  4770  ssunsn2  4792  n0snor2el  4796  preq12nebg  4825  opthprneg  4827  elpreqprlem  4828  dfopif  4832  csbuni  4902  disjord  5098  sbcbr  5165  unisn2  5274  intabs  5304  class2set  5315  dtruALT2  5330  snexALT  5343  dtruALT  5348  axprlem3  5385  snex  5393  exneq  5397  dtruOLD  5403  copsexgw  5452  copsexg  5453  snopeqop  5468  csbopab  5517  0nelopabOLD  5530  dfid3  5539  csbxp  5736  csbres  5945  csbima12  6036  soirri  6085  csbrn  6160  dmsnopss  6171  dmsnsnsn  6177  opswap  6186  unixpid  6241  predres  6298  nsuceq0  6405  ordsssuc2  6413  iotassuni  6473  iotaex  6474  iotassuniOLD  6480  iotaexOLD  6481  csbiota  6494  dffv3  6843  fvrn0  6877  ndmfv  6882  elfv2ex  6893  fveqres  6894  csbfv12  6895  csbfv  6897  dffv2  6941  fvco4i  6947  fvmptss  6965  fvmptex  6967  fvmptss2  6978  fvmptrabfv  6984  f0cli  7053  fvunsn  7130  fconst5  7160  csbriota  7334  riotassuni  7359  oprabidw  7393  csbov123  7404  csbov  7405  fvmptopab  7416  fvmptopabOLD  7417  brfvopab  7419  elimdelov  7458  ovif12  7461  ndmovcl  7544  ndmovord  7549  elovmpt3imp  7615  difsnexi  7700  ordsuc  7753  ordsucOLD  7754  ordsucelsuc  7762  1stval  7928  2ndval  7929  1st2val  7954  2nd2val  7955  el2mpocsbcl  8022  bropopvvv  8027  bropfvvvvlem  8028  bropfvvvv  8029  suppimacnv  8110  suppssdm  8113  ressuppss  8119  suppun  8120  extmptsuppeq  8124  funsssuppss  8126  fczsupp0  8129  suppss  8130  suppssOLD  8131  suppssov1  8134  suppss2  8136  suppssfv  8138  suppco  8142  mpoxopynvov0  8154  mpoxopoveqd  8157  pwuninel  8211  smofvon2  8307  om0x  8470  mapssfset  8796  brdomg  8903  brdomgOLD  8904  snfi  8995  sdomirr  9065  domunsn  9078  2pwuninel  9083  unfi  9123  cnvfi  9131  snnen2oOLD  9178  suppeqfsuppbi  9328  fsuppun  9333  funsnfsupp  9338  fipwuni  9371  oicl  9474  oif  9475  wemapso2  9498  card2on  9499  en2lp  9551  ttrclselem1  9670  tctr  9685  r1tr  9721  rankdmr1  9746  r1pw  9790  r1pwALT  9791  rankuni  9808  scottex  9830  cardidm  9904  alephcard  10015  alephnbtwn  10016  cfub  10194  cardcf  10197  cflecard  10198  cfle  10199  cflim2  10208  cfidm  10220  isf32lem9  10306  itunisuc  10364  itunitc1  10365  itunitc  10366  ituniiun  10367  axcc2lem  10381  alephreg  10527  pwcfsdom  10528  cfpwsdom  10529  axunndlem1  10540  axpownd  10546  tskmcl  10786  addcompi  10839  addasspi  10840  mulcompi  10841  mulasspi  10842  distrpi  10843  addnidpi  10846  nlt1pi  10851  addcompq  10895  addcomnq  10896  mulcompq  10897  mulcomnq  10898  adderpq  10901  mulerpq  10902  addassnq  10903  mulassnq  10904  distrnq  10906  genpass  10954  addcompr  10966  mulcompr  10968  distrpr  10973  ltexprlem7  10987  addcomsr  11032  addasssr  11033  mulcomsr  11034  mulasssr  11035  distrsr  11036  uzssz  12793  uzwo  12845  nn01to3  12875  xnn0xaddcl  13164  elixx3g  13287  iooid  13302  elfz2  13441  injresinjlem  13702  injresinj  13703  fleqceilz  13769  modifeq2int  13848  modfzo0difsn  13858  addmodlteq  13861  ltweuz  13876  fzofi  13889  fsuppmapnn0fiubex  13907  hashrabrsn  14282  hashrabsn01  14283  hashrabsn1  14284  elprchashprn2  14306  hashss  14319  hashsn01  14326  hash1snb  14329  hashgt12el  14332  hashgt12el2  14333  hashgt23el  14334  hashfzp1  14341  hashfundm  14352  hash2pwpr  14387  hashge2el2dif  14391  ffz0iswrd  14441  ccatsymb  14482  swrd00  14544  swrd0  14558  swrdwrdsymb  14562  pfx00  14574  pfx0  14575  repswswrd  14684  0csh0  14693  cshwcl  14698  cshwidxmod  14703  repswcshw  14712  cshw1  14722  s3sndisj  14864  s3iunsndisj  14865  xptrrel  14877  trclfvcotrg  14913  relexpfld  14946  reusq0  15359  modfsummods  15689  dvdsaddre2b  16200  gcdaddmlem  16415  prm23ge5  16698  pcmptcl  16774  prmgaplem5  16938  prmgaplem6  16939  cshwshash  16988  strle1  17041  strfvss  17070  strfvi  17073  setsnid  17092  setsnidOLD  17093  ressbas  17129  ressbasOLD  17130  ressbasssg  17131  ressbasssOLD  17134  resseqnbas  17136  resslemOLD  17137  ress0  17138  ressress  17143  0rest  17325  firest  17328  topnval  17330  xpsaddlem  17469  xpsvsca  17473  homffval  17584  comfffval  17592  oppchomfval  17608  oppchomfvalOLD  17609  oppcbas  17613  oppcbasOLD  17614  fullfunc  17807  fthfunc  17808  natfval  17847  fucbas  17862  fuchom  17863  fuchomOLD  17864  arwval  17943  coafval  17964  xpcbas  18080  xpchomfval  18081  xpccofval  18084  oduval  18191  oduleval  18192  lubfun  18255  glbfun  18268  odujoin  18311  odumeet  18313  ipopos  18439  plusffval  18517  grpidval  18530  gsum0  18553  frmdplusg  18678  frmd0  18684  efmndbas  18695  efmndbasabf  18696  efmndplusg  18704  mgm2nsgrplem2  18743  mgm2nsgrplem3  18744  sgrp2rid2  18750  dfgrp2e  18790  grpinvfval  18803  grpinvfvalALT  18804  grpinvfvi  18807  grpsubfval  18808  grpsubfvalALT  18809  mulgfval  18888  mulgfvalALT  18889  mulgfvi  18892  cntrval  19113  oppgval  19139  oppgplusfval  19140  symgval  19164  snsymgefmndeq  19190  psgnfval  19296  odfval  19328  odfvalALT  19329  oppglsm  19438  efgval  19513  mgpval  19913  mgpplusg  19914  ringidval  19929  opprval  20064  opprmulfval  20065  dvdsrval  20088  invrfval  20116  dvrfval  20127  staffval  20362  scaffval  20397  rlmval  20719  rlmsca2  20729  2idlval  20762  rrgval  20794  zrhval  20945  zlmlem  20954  zlmlemOLD  20955  zlmvsca  20963  chrval  20965  evpmss  21027  psgndiflemB  21041  ipffval  21089  thlbas  21137  thlbasOLD  21138  thlle  21139  thlleOLD  21140  thloc  21142  pjfval  21149  dsmmval2  21179  asclfval  21319  psrplusg  21386  psrmulr  21389  psrvscafval  21395  mplval  21434  mplcoe3  21476  evlval  21542  psr1val  21594  vr1val  21600  ply1val  21602  ply1basfvi  21649  ply1plusgfvi  21650  psr1sca2  21659  ply1sca2  21662  ply1ascl  21666  cply1mul  21702  gsummoncoe1  21712  evl1fval  21731  evl1fval1  21734  mamufacex  21775  mavmulsolcl  21937  marrepfval  21946  marepvfval  21951  submafval  21965  mdetfval  21972  mdetfval1  21976  mdetunilem7  22004  mdetunilem8  22005  madufval  22023  minmar1fval  22032  mp2pm2mplem4  22195  toponsspwpw  22308  tgdif0  22379  indislem  22387  resstopn  22574  iocpnfordt  22603  icomnfordt  22604  hmeofval  23146  ussval  23648  nmfval  23981  nghmfval  24123  pcofval  24410  tcphval  24619  ioombl  24966  ibladdlem  25221  itgaddlem1  25224  iblabs  25230  dvbsss  25303  perfdvf  25304  mdegfval  25464  deg1fval  25482  deg1fvi  25487  uc1pval  25541  mon1pval  25543  2irrexpq  26122  lgsqrmodndvds  26738  gausslemma2dlem1a  26750  2lgs  26792  2sqreultblem  26833  2sqreunnltblem  26836  newval  27228  leftval  27236  rightval  27237  lltropt  27245  oldssmade  27250  lrold  27269  ttglem  27882  ttglemOLD  27883  axcontlem12  27987  vtxval  28014  iedgval  28015  edgval  28063  usgr1v  28267  nbuhgr  28354  nbumgr  28358  uhgrnbgr0nb  28365  nbgr1vtx  28369  nbgrnself2  28371  nbusgrvtxm1  28390  sizusglecusg  28474  g0wlk0  28663  wlkreslem  28680  lfgrwlkprop  28698  wwlks  28843  wwlksn  28845  wspthsn  28856  iswwlksnon  28861  iswspthsnon  28864  0enwwlksnge1  28872  wwlksnfi  28914  clwwlk  28990  umgrclwwlkge2  28998  clwlkclwwlklem2a4  29004  clwwlkn  29033  clwwlknonmpo  29096  clwwlknon  29097  clwwlk0on0  29099  clwwlknon1le1  29108  1conngr  29201  eupth2lem3lem7  29241  frgr1v  29278  nfrgr2v  29279  1to2vfriswmgr  29286  2wspmdisj  29344  frgrreggt1  29400  frgrreg  29401  frgrregord013  29402  frgrogt3nreg  29404  friendship  29406  avril1  29470  vafval  29608  bafval  29609  smfval  29610  vsfval  29638  bcsiALT  30184  resvsca  32192  resvlem  32193  resvlemOLD  32194  cntnevol  32916  signsw0glem  33254  bnj1189  33710  fmlafvel  34066  gonan0  34073  satffun  34090  mvtval  34181  mexval  34183  mexval2  34184  mdvval  34185  mrsubfval  34189  mrsubrn  34194  msubfval  34205  elmsubrn  34209  msubrn  34210  mvhfval  34214  mpstval  34216  msrfval  34218  mstaval  34225  mppsval  34253  mthmval  34256  dfrdg3  34457  fvsingle  34581  unisnif  34586  funpartfv  34606  fullfunfv  34608  linedegen  34804  bj-ax6e  35208  axc11n11r  35224  bj-ax12v3ALT  35227  bj-sbsb  35378  bj-nfcsym  35442  bj-snex  35579  bj-restsnid  35631  bj-inftyexpitaudisj  35749  bj-inftyexpidisj  35754  finxpreclem4  35938  finxp00  35946  isinf2  35949  wl-nfs1t  36069  matunitlindflem1  36147  itg2addnclem  36202  ibladdnclem  36207  itgaddnclem1  36209  iblabsnc  36215  iblmulc2nc  36216  ftc1anclem8  36231  ismgmOLD  36382  tsbi1  36665  tsbi2  36666  ac6s6  36704  equid1  37434  ax12fromc15  37440  equid1ALT  37460  dvelimf-o  37464  ax12inda2ALT  37481  ax12inda2  37482  sn-axprlem3  40710  fsuppind  40823  mzpmfp  41128  itgocn  41549  mendbas  41569  mendplusgfval  41570  mendmulrfval  41572  mendsca  41574  mendvscafval  41575  arearect  41607  areaquad  41608  fpwfvss  41806  safesnsupfidom1o  41811  sn1dom  41920  or3or  42417  uneqsn  42419  addcomgi  42858  ax6e2ndeq  42963  2sb5ndVD  43314  2sb5ndALT  43336  sqwvfoura  44589  sqwvfourb  44590  fourierswlem  44591  fouriersw  44592  hspdifhsp  44977  hspmbllem2  44988  hspmbl  44990  et-ltneverrefl  45232  tz6.12-afv  45525  ndmaovcl  45555  tz6.12-afv2  45592  otiunsndisjX  45631  fvmptrab  45644  nltle2tri  45665  fzopredsuc  45675  iccpartiltu  45734  iccpartigtl  45735  iccpartlt  45736  icceuelpartlem  45747  iccpartnel  45750  elsprel  45787  sprssspr  45793  sprsymrelfvlem  45802  prprelprb  45829  prprspr2  45830  fmtnoprmfac1  45877  fmtnoprmfac2  45879  prmdvdsfmtnof1lem2  45897  prminf2  45900  lighneallem4  45922  requad1  45934  requad2  45935  evenprm2  46026  even3prm2  46031  fpprbasnn  46041  stgoldbwt  46088  upwlkbprop  46160  nzerooringczr  46490  pgrpgt2nabl  46562  suppmptcfin  46575  linc1  46626  lindslinindsimp2lem5  46663  1aryenef  46851  2aryenef  46862  reorelicc  46916  rrxsphere  46954  fvconst0ci  47045  fvconstdomi  47046  setrec2lem1  47258  setrec2mpt  47262