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  380  pm5.18  383  biass  386  pm2.61ian  809  ecase3  1029  4cases  1038  pm4.42  1051  ifpid  1075  elimh  1082  3ecase  1473  norass  1535  ax6e  2384  ax12  2424  exdistrf  2448  equvini  2456  ax12vALT  2470  2ax6e  2472  sb1  2480  sb2  2481  sb1OLD  2483  sb4a  2485  dfsb1  2486  dfsb2  2498  sbcom3  2511  sbco2  2516  sbco3  2518  sb9  2524  nfsbOLD  2529  eujustALT  2573  pm2.61ine  3029  ralcom2  3291  eueq2  3646  moeq3  3648  mo2icl  3650  sbc2or  3726  unineq  4212  csb0  4342  sbcel12  4343  sbcne12  4347  sbcel2  4350  csbidm  4365  csbun  4373  csbin  4374  ralidmOLD  4447  csbdif  4459  ifsb  4473  ifid  4500  ifnot  4512  ifan  4513  ifor  4514  csbif  4517  elimhyp  4525  elimhyp2v  4526  elimhyp3v  4527  elimhyp4v  4528  elimdhyp  4530  keephyp2v  4532  keephyp3v  4533  rmosn  4656  rabsnif  4660  tppreqb  4739  ssunsn2  4761  n0snor2el  4765  preq12nebg  4794  opthprneg  4796  elpreqprlem  4797  dfopifOLD  4802  csbuni  4871  disjord  5063  sbcbr  5130  unisn2  5237  intabs  5267  class2set  5277  dtruALT2  5294  snexALT  5307  dtruALT  5312  axprlem3  5349  snex  5355  dtru  5360  copsexgw  5405  copsexg  5406  snopeqop  5421  csbopab  5469  0nelopabOLD  5482  dfid3  5493  csbxp  5687  csbres  5897  csbima12  5990  soirri  6036  csbrn  6111  dmsnopss  6122  dmsnsnsn  6128  opswap  6137  unixpid  6191  predres  6246  nsuceq0  6350  ordsssuc2  6358  iotassuni  6416  iotaex  6417  csbiota  6430  dffv3  6779  fvrn0  6811  ndmfv  6813  elfv2ex  6824  fveqres  6825  csbfv12  6826  csbfv  6828  dffv2  6872  fvco4i  6878  fvmptss  6896  fvmptex  6898  fvmptss2  6909  fvmptrabfv  6915  f0cli  6983  fvunsn  7060  fconst5  7090  csbriota  7257  riotassuni  7282  oprabidw  7315  csbov123  7326  csbov  7327  fvmptopab  7338  fvmptopabOLD  7339  brfvopab  7341  elimdelov  7380  ovif12  7383  ndmovcl  7466  ndmovord  7471  elovmpt3imp  7535  difsnexi  7620  ordsuc  7670  ordsucelsuc  7678  1stval  7842  2ndval  7843  1st2val  7868  2nd2val  7869  el2mpocsbcl  7934  bropopvvv  7939  bropfvvvvlem  7940  bropfvvvv  7941  suppimacnv  7999  suppssdm  8002  ressuppss  8008  suppun  8009  extmptsuppeq  8013  funsssuppss  8015  fczsupp0  8018  suppss  8019  suppssOLD  8020  suppssov1  8023  suppss2  8025  suppssfv  8027  suppco  8031  mpoxopynvov0  8043  mpoxopoveqd  8046  pwuninel  8100  smofvon2  8196  om0x  8358  mapssfset  8648  brdomg  8755  brdomgOLD  8756  snfi  8843  sdomirr  8910  domunsn  8923  2pwuninel  8928  unfi  8964  cnvfi  8972  snnen2oOLD  9019  suppeqfsuppbi  9151  fsuppun  9156  funsnfsupp  9161  fipwuni  9194  oicl  9297  oif  9298  wemapso2  9321  card2on  9322  en2lp  9373  ttrclselem1  9492  tctr  9507  r1tr  9543  rankdmr1  9568  r1pw  9612  r1pwALT  9613  rankuni  9630  scottex  9652  cardidm  9726  alephcard  9835  alephnbtwn  9836  cfub  10014  cardcf  10017  cflecard  10018  cfle  10019  cflim2  10028  cfidm  10040  isf32lem9  10126  itunisuc  10184  itunitc1  10185  itunitc  10186  ituniiun  10187  axcc2lem  10201  alephreg  10347  pwcfsdom  10348  cfpwsdom  10349  axunndlem1  10360  axpownd  10366  tskmcl  10606  addcompi  10659  addasspi  10660  mulcompi  10661  mulasspi  10662  distrpi  10663  addnidpi  10666  nlt1pi  10671  addcompq  10715  addcomnq  10716  mulcompq  10717  mulcomnq  10718  adderpq  10721  mulerpq  10722  addassnq  10723  mulassnq  10724  distrnq  10726  genpass  10774  addcompr  10786  mulcompr  10788  distrpr  10793  ltexprlem7  10807  addcomsr  10852  addasssr  10853  mulcomsr  10854  mulasssr  10855  distrsr  10856  uzssz  12612  uzwo  12660  nn01to3  12690  xnn0xaddcl  12978  elixx3g  13101  iooid  13116  elfz2  13255  injresinjlem  13516  injresinj  13517  fleqceilz  13583  modifeq2int  13662  modfzo0difsn  13672  addmodlteq  13675  ltweuz  13690  fzofi  13703  fsuppmapnn0fiubex  13721  hashrabrsn  14096  hashrabsn01  14097  hashrabsn1  14098  elprchashprn2  14120  hashss  14133  hashsn01  14140  hash1snb  14143  hashgt12el  14146  hashgt12el2  14147  hashgt23el  14148  hashfzp1  14155  hash2pwpr  14199  hashge2el2dif  14203  ffz0iswrd  14253  ccatsymb  14296  swrd00  14366  swrd0  14380  swrdwrdsymb  14384  pfx00  14396  pfx0  14397  repswswrd  14506  0csh0  14515  cshwcl  14520  cshwidxmod  14525  repswcshw  14534  cshw1  14544  s3sndisj  14687  s3iunsndisj  14688  xptrrel  14700  trclfvcotrg  14736  relexpfld  14769  reusq0  15183  modfsummods  15514  dvdsaddre2b  16025  gcdaddmlem  16240  prm23ge5  16525  pcmptcl  16601  prmgaplem5  16765  prmgaplem6  16766  cshwshash  16815  strle1  16868  strfvss  16897  strfvi  16900  setsnid  16919  setsnidOLD  16920  ressbas  16956  ressbasOLD  16957  ressbasss  16959  resseqnbas  16960  resslemOLD  16961  ress0  16962  ressress  16967  0rest  17149  firest  17152  topnval  17154  xpsaddlem  17293  xpsvsca  17297  homffval  17408  comfffval  17416  oppchomfval  17432  oppchomfvalOLD  17433  oppcbas  17437  oppcbasOLD  17438  fullfunc  17631  fthfunc  17632  natfval  17671  fucbas  17686  fuchom  17687  fuchomOLD  17688  arwval  17767  coafval  17788  xpcbas  17904  xpchomfval  17905  xpccofval  17908  oduval  18015  oduleval  18016  lubfun  18079  glbfun  18092  odujoin  18135  odumeet  18137  ipopos  18263  plusffval  18341  grpidval  18354  gsum0  18377  frmdplusg  18502  frmd0  18508  efmndbas  18519  efmndbasabf  18520  efmndplusg  18528  mgm2nsgrplem2  18567  mgm2nsgrplem3  18568  sgrp2rid2  18574  dfgrp2e  18614  grpinvfval  18627  grpinvfvalALT  18628  grpinvfvi  18631  grpsubfval  18632  grpsubfvalALT  18633  mulgfval  18711  mulgfvalALT  18712  mulgfvi  18715  cntrval  18934  oppgval  18960  oppgplusfval  18961  symgval  18985  snsymgefmndeq  19011  psgnfval  19117  odfval  19149  odfvalALT  19150  oppglsm  19256  efgval  19332  mgpval  19732  mgpplusg  19733  ringidval  19748  opprval  19872  opprmulfval  19873  dvdsrval  19896  invrfval  19924  dvrfval  19935  staffval  20116  scaffval  20150  rlmval  20470  rlmsca2  20480  2idlval  20513  rrgval  20567  zrhval  20718  zlmlem  20727  zlmlemOLD  20728  zlmvsca  20736  chrval  20738  evpmss  20800  psgndiflemB  20814  ipffval  20862  thlbas  20910  thlbasOLD  20911  thlle  20912  thlleOLD  20913  thloc  20915  pjfval  20922  dsmmval2  20952  asclfval  21092  psrplusg  21159  psrmulr  21162  psrvscafval  21168  mplval  21206  mplcoe3  21248  evlval  21314  psr1val  21366  vr1val  21372  ply1val  21374  ply1basfvi  21421  ply1plusgfvi  21422  psr1sca2  21431  ply1sca2  21434  ply1ascl  21438  cply1mul  21474  gsummoncoe1  21484  evl1fval  21503  evl1fval1  21506  mamufacex  21547  mavmulsolcl  21709  marrepfval  21718  marepvfval  21723  submafval  21737  mdetfval  21744  mdetfval1  21748  mdetunilem7  21776  mdetunilem8  21777  madufval  21795  minmar1fval  21804  mp2pm2mplem4  21967  toponsspwpw  22080  tgdif0  22151  indislem  22159  resstopn  22346  iocpnfordt  22375  icomnfordt  22376  hmeofval  22918  ussval  23420  nmfval  23753  nghmfval  23895  pcofval  24182  tcphval  24391  ioombl  24738  ibladdlem  24993  itgaddlem1  24996  iblabs  25002  dvbsss  25075  perfdvf  25076  mdegfval  25236  deg1fval  25254  deg1fvi  25259  uc1pval  25313  mon1pval  25315  2irrexpq  25894  lgsqrmodndvds  26510  gausslemma2dlem1a  26522  2lgs  26564  2sqreultblem  26605  2sqreunnltblem  26608  ttglem  27247  ttglemOLD  27248  axcontlem12  27352  vtxval  27379  iedgval  27380  edgval  27428  usgr1v  27632  nbuhgr  27719  nbumgr  27723  uhgrnbgr0nb  27730  nbgr1vtx  27734  nbgrnself2  27736  nbusgrvtxm1  27755  sizusglecusg  27839  g0wlk0  28028  wlkreslem  28046  lfgrwlkprop  28064  wwlks  28209  wwlksn  28211  wspthsn  28222  iswwlksnon  28227  iswspthsnon  28230  0enwwlksnge1  28238  wwlksnfi  28280  clwwlk  28356  umgrclwwlkge2  28364  clwlkclwwlklem2a4  28370  clwwlkn  28399  clwwlknonmpo  28462  clwwlknon  28463  clwwlk0on0  28465  clwwlknon1le1  28474  1conngr  28567  eupth2lem3lem7  28607  frgr1v  28644  nfrgr2v  28645  1to2vfriswmgr  28652  2wspmdisj  28710  frgrreggt1  28766  frgrreg  28767  frgrregord013  28768  frgrogt3nreg  28770  friendship  28772  avril1  28836  vafval  28974  bafval  28975  smfval  28976  vsfval  29004  bcsiALT  29550  resvsca  31538  resvlem  31539  resvlemOLD  31540  cntnevol  32205  signsw0glem  32541  bnj1189  32998  hashfundm  33083  fmlafvel  33356  gonan0  33363  satffun  33380  mvtval  33471  mexval  33473  mexval2  33474  mdvval  33475  mrsubfval  33479  mrsubrn  33484  msubfval  33495  elmsubrn  33499  msubrn  33500  mvhfval  33504  mpstval  33506  msrfval  33508  mstaval  33515  mppsval  33543  mthmval  33546  dfrdg3  33781  newval  34048  leftval  34056  rightval  34057  oldssmade  34069  lrold  34086  fvsingle  34231  unisnif  34236  funpartfv  34256  fullfunfv  34258  linedegen  34454  bj-ax6e  34858  axc11n11r  34874  bj-ax12v3ALT  34877  bj-dtru  35008  bj-sbsb  35029  bj-nfcsym  35093  bj-restsnid  35267  bj-inftyexpitaudisj  35385  bj-inftyexpidisj  35390  finxpreclem4  35574  finxp00  35582  isinf2  35585  wl-nfs1t  35705  matunitlindflem1  35782  itg2addnclem  35837  ibladdnclem  35842  itgaddnclem1  35844  iblabsnc  35850  iblmulc2nc  35851  ftc1anclem8  35866  ismgmOLD  36017  tsbi1  36300  tsbi2  36301  ac6s6  36339  equid1  36920  ax12fromc15  36926  equid1ALT  36946  dvelimf-o  36950  ax12inda2ALT  36967  ax12inda2  36968  sn-axprlem3  40193  sn-dtru  40195  sn-iotassuni  40203  sn-iotaex  40204  fsuppind  40286  mzpmfp  40576  itgocn  40996  mendbas  41016  mendplusgfval  41017  mendmulrfval  41019  mendsca  41021  mendvscafval  41022  arearect  41053  areaquad  41054  sn1dom  41140  or3or  41638  uneqsn  41640  addcomgi  42081  ax6e2ndeq  42186  2sb5ndVD  42537  2sb5ndALT  42559  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  hspdifhsp  44161  hspmbllem2  44172  hspmbl  44174  tz6.12-afv  44676  ndmaovcl  44706  tz6.12-afv2  44743  otiunsndisjX  44782  fvmptrab  44795  nltle2tri  44816  fzopredsuc  44826  iccpartiltu  44885  iccpartigtl  44886  iccpartlt  44887  icceuelpartlem  44898  iccpartnel  44901  elsprel  44938  sprssspr  44944  sprsymrelfvlem  44953  prprelprb  44980  prprspr2  44981  fmtnoprmfac1  45028  fmtnoprmfac2  45030  prmdvdsfmtnof1lem2  45048  prminf2  45051  lighneallem4  45073  requad1  45085  requad2  45086  evenprm2  45177  even3prm2  45182  fpprbasnn  45192  stgoldbwt  45239  upwlkbprop  45311  nzerooringczr  45641  pgrpgt2nabl  45713  suppmptcfin  45726  linc1  45777  lindslinindsimp2lem5  45814  1aryenef  46002  2aryenef  46013  reorelicc  46067  rrxsphere  46105  fvconst0ci  46197  fvconstdomi  46198  setrec2lem1  46410  et-ltneverrefl  46521