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  2387  ax12  2427  exdistrf  2451  equvini  2459  ax12vALT  2473  2ax6e  2475  sb1  2482  sb2  2483  sb4a  2484  dfsb1  2485  dfsb2  2497  sbcom3  2510  sbco2  2515  sbco3  2517  sb9  2523  eujustALT  2572  pm2.61ine  3015  ralcom2  3339  eueq2  3656  moeq3  3658  mo2icl  3660  sbc2or  3737  unineq  4228  csb0  4350  sbcel12  4351  sbcne12  4355  sbcel2  4358  csbidm  4373  csbun  4381  csbin  4382  csbdif  4465  ifsb  4480  ifid  4507  ifnot  4519  ifan  4520  ifor  4521  csbif  4524  elimhyp  4532  elimhyp2v  4533  elimhyp3v  4534  elimhyp4v  4535  elimdhyp  4537  keephyp2v  4539  keephyp3v  4540  rmosn  4663  rabsnif  4667  tppreqb  4750  ssunsn2  4770  n0snor2el  4776  preq12nebg  4806  opthprneg  4808  elpreqprlem  4809  dfopif  4813  csbuni  4880  disjord  5074  sbcbr  5140  unisn2  5247  intabs  5290  class2set  5296  dtruALT2  5312  snexALT  5325  dtruALT  5330  axprlem3  5367  axprlem3OLD  5371  axprglem  5378  axprg  5379  snexOLD  5384  exneq  5388  copsexgwOLD  5444  copsexg  5445  snopeqop  5460  csbopab  5510  dfid3  5529  csbxp  5732  csbres  5947  csbima12  6044  soirri  6089  csbrn  6167  dmsnopss  6178  dmsnsnsn  6184  opswap  6193  unixpid  6248  predres  6303  nsuceq0  6408  ordsssuc2  6416  iotassuni  6473  iotaex  6474  csbiota  6491  dffv3  6836  fvrn0  6868  ndmfv  6872  elfv2ex  6883  fveqres  6884  csbfv12  6885  csbfv  6887  dffv2  6935  fvco4i  6941  fvmptss  6960  fvmptex  6962  fvmptss2  6974  fvmptrabfv  6980  f0cli  7050  fvunsn  7134  fconst5  7161  csbriota  7339  riotassuni  7364  oprabidw  7398  csbov123  7411  csbov  7412  fvmptopab  7422  brfvopab  7424  elimdelov  7463  ovif12  7467  ifmpt2v  7469  ndmovcl  7552  ndmovord  7557  elovmpt3imp  7624  difsnexi  7715  ordsuc  7765  ordsucelsuc  7773  1stval  7944  2ndval  7945  1st2val  7970  2nd2val  7971  el2mpocsbcl  8035  bropopvvv  8040  bropfvvvvlem  8041  bropfvvvv  8042  suppimacnv  8124  suppssdm  8127  ressuppss  8133  suppun  8134  extmptsuppeq  8138  funsssuppss  8140  fczsupp0  8143  suppss  8144  suppss2  8150  suppssfv  8152  suppco  8156  mpoxopynvov0  8168  mpoxopoveqd  8171  pwuninel  8225  smofvon2  8296  om0x  8454  mapssfset  8798  brdomg  8905  snfi  8990  sdomirr  9052  domunsn  9065  2pwuninel  9070  unfi  9105  cnvfi  9110  suppeqfsuppbi  9292  fsuppun  9300  funsnfsupp  9305  fipwuni  9339  oicl  9444  oif  9445  wemapso2  9468  card2on  9469  en2lp  9527  ttrclselem1  9646  tctr  9659  r1tr  9700  rankdmr1  9725  r1pw  9769  r1pwALT  9770  rankuni  9787  scottex  9809  cardidm  9883  alephcard  9992  alephnbtwn  9993  cfub  10171  cardcf  10174  cflecard  10175  cfle  10176  cflim2  10185  cfidm  10197  isf32lem9  10283  itunisuc  10341  itunitc1  10342  itunitc  10343  ituniiun  10344  axcc2lem  10358  alephreg  10505  pwcfsdom  10506  cfpwsdom  10507  axunndlem1  10518  axpownd  10524  tskmcl  10764  addcompi  10817  addasspi  10818  mulcompi  10819  mulasspi  10820  distrpi  10821  addnidpi  10824  nlt1pi  10829  addcompq  10873  addcomnq  10874  mulcompq  10875  mulcomnq  10876  adderpq  10879  mulerpq  10880  addassnq  10881  mulassnq  10882  distrnq  10884  genpass  10932  addcompr  10944  mulcompr  10946  distrpr  10951  ltexprlem7  10965  addcomsr  11010  addasssr  11011  mulcomsr  11012  mulasssr  11013  distrsr  11014  indval0  12163  uzssz  12809  uzwo  12861  nn01to3  12891  xnn0xaddcl  13187  elixx3g  13311  iooid  13326  elfz2  13468  injresinjlem  13745  injresinj  13746  fleqceilz  13813  modifeq2int  13895  modfzo0difsn  13905  addmodlteq  13908  ltweuz  13923  fzofi  13936  fsuppmapnn0fiubex  13954  hashrabrsn  14334  hashrabsn01  14335  hashrabsn1  14336  elprchashprn2  14358  hashss  14371  hashsn01  14378  hash1snb  14381  hashgt12el  14384  hashgt12el2  14385  hashgt23el  14386  hashfzp1  14393  hashfundm  14404  hash2pwpr  14438  hashge2el2dif  14442  hash3tpde  14455  ffz0iswrd  14503  ccatsymb  14545  swrd00  14607  swrd0  14621  swrdwrdsymb  14625  pfx00  14637  pfx0  14638  repswswrd  14746  0csh0  14755  cshwcl  14760  cshwidxmod  14765  repswcshw  14774  cshw1  14784  s3sndisj  14929  s3iunsndisj  14930  xptrrel  14942  trclfvcotrg  14978  relexpfld  15011  reusq0  15427  modfsummods  15756  dvdsaddre2b  16276  gcdaddmlem  16493  prm23ge5  16786  pcmptcl  16862  prmgaplem5  17026  prmgaplem6  17027  cshwshash  17075  strle1  17128  strfvss  17157  strfvi  17160  setsnid  17178  ressbas  17206  ressbasssg  17207  ressbasssOLD  17210  resseqnbas  17212  ress0  17213  ressress  17217  0rest  17392  firest  17395  topnval  17397  xpsaddlem  17537  xpsvsca  17541  homffval  17656  comfffval  17664  oppchomfval  17680  oppcbas  17684  fullfunc  17875  fthfunc  17876  natfval  17916  fucbas  17930  fuchom  17931  arwval  18010  coafval  18031  xpcbas  18144  xpchomfval  18145  xpccofval  18148  oduval  18254  oduleval  18255  lubfun  18316  glbfun  18329  odujoin  18372  odumeet  18374  ipopos  18502  plusffval  18614  grpidval  18629  gsum0  18652  frmdplusg  18822  frmd0  18828  efmndbas  18839  efmndbasabf  18840  efmndplusg  18848  mgm2nsgrplem2  18890  mgm2nsgrplem3  18891  sgrp2rid2  18897  dfgrp2e  18939  grpinvfval  18954  grpinvfvalALT  18955  grpinvfvi  18958  grpsubfval  18959  grpsubfvalALT  18960  mulgfval  19045  mulgfvalALT  19046  mulgfvi  19049  cntrval  19294  oppgval  19322  oppgplusfval  19323  symgval  19346  snsymgefmndeq  19370  psgnfval  19475  odfval  19507  odfvalALT  19508  oppglsm  19617  efgval  19692  mgpval  20124  mgpplusg  20125  ringidval  20164  opprval  20318  opprmulfval  20319  dvdsrval  20341  invrfval  20369  dvrfval  20382  rrgval  20674  staffval  20818  scaffval  20875  rlmval  21186  rlmsca2  21194  2idlval  21249  nzerooringczr  21460  zrhval  21487  zlmlem  21496  zlmvsca  21501  chrval  21503  evpmss  21566  psgndiflemB  21580  ipffval  21628  thlbas  21676  thlle  21677  thloc  21679  pjfval  21686  dsmmval2  21716  asclfval  21858  psrplusg  21916  psrmulr  21921  psrvscafval  21927  mplval  21967  mplcoe3  22016  evlval  22078  psr1val  22149  vr1val  22155  ply1val  22157  ply1basfvi  22204  ply1plusgfvi  22205  psr1sca2  22214  ply1sca2  22217  ply1ascl  22223  cply1mul  22261  gsummoncoe1  22273  evl1fval  22293  evl1fval1  22296  mamufacex  22361  mavmulsolcl  22516  marrepfval  22525  marepvfval  22530  submafval  22544  mdetfval  22551  mdetfval1  22555  mdetunilem7  22583  mdetunilem8  22584  madufval  22602  minmar1fval  22611  mp2pm2mplem4  22774  toponsspwpw  22887  tgdif0  22957  indislem  22965  resstopn  23151  iocpnfordt  23180  icomnfordt  23181  hmeofval  23723  ussval  24224  nmfval  24553  nghmfval  24687  pcofval  24977  tcphval  25185  ioombl  25532  ibladdlem  25787  itgaddlem1  25790  iblabs  25796  dvbsss  25869  perfdvf  25870  mdegfval  26027  deg1fval  26045  deg1fvi  26050  uc1pval  26105  mon1pval  26107  2irrexpq  26695  lgsqrmodndvds  27316  gausslemma2dlem1a  27328  2lgs  27370  2sqreultblem  27411  2sqreunnltblem  27414  newval  27827  leftval  27841  rightval  27842  lltr  27854  oldssmade  27859  oldss  27862  lrold  27889  ttglem  28944  axcontlem12  29044  vtxval  29069  iedgval  29070  edgval  29118  usgr1v  29325  nbuhgr  29412  nbumgr  29416  uhgrnbgr0nb  29423  nbgr1vtx  29427  nbgrnself2  29429  nbusgrvtxm1  29448  sizusglecusg  29532  g0wlk0  29719  wlkreslem  29736  lfgrwlkprop  29754  wwlks  29903  wwlksn  29905  wspthsn  29916  iswwlksnon  29921  iswspthsnon  29924  0enwwlksnge1  29932  wwlksnfi  29974  clwwlk  30053  umgrclwwlkge2  30061  clwlkclwwlklem2a4  30067  clwwlkn  30096  clwwlknonmpo  30159  clwwlknon  30160  clwwlk0on0  30162  clwwlknon1le1  30171  1conngr  30264  eupth2lem3lem7  30304  frgr1v  30341  nfrgr2v  30342  1to2vfriswmgr  30349  2wspmdisj  30407  frgrreggt1  30463  frgrreg  30464  frgrregord013  30465  frgrogt3nreg  30467  friendship  30469  avril1  30533  vafval  30674  bafval  30675  smfval  30676  vsfval  30704  bcsiALT  31250  of0r  32752  fracval  33365  fracbas  33366  resvsca  33392  resvlem  33393  cntnevol  34372  signsw0glem  34697  bnj1189  35151  r1wf  35239  noinfepregs  35277  fmlafvel  35567  gonan0  35574  satffun  35591  mvtval  35682  mexval  35684  mexval2  35685  mdvval  35686  mrsubfval  35690  mrsubrn  35695  msubfval  35706  elmsubrn  35710  msubrn  35711  mvhfval  35715  mpstval  35717  msrfval  35719  mstaval  35726  mppsval  35754  mthmval  35757  antnestlaw2  35874  dfrdg3  35976  fvsingle  36100  unisnif  36105  funpartfv  36127  fullfunfv  36129  linedegen  36325  axtcond  36660  csbttc  36691  mh-setindnd  36719  bj-ax6e  36962  axc11n11r  36980  bj-ax12v3ALT  36983  bj-sbsb  37144  bj-nfcsym  37206  bj-snex  37342  bj-restsnid  37399  bj-inftyexpitaudisj  37519  bj-inftyexpidisj  37524  finxpreclem4  37710  finxp00  37718  isinf2  37721  wl-nfs1t  37862  matunitlindflem1  37937  itg2addnclem  37992  ibladdnclem  37997  itgaddnclem1  37999  iblabsnc  38005  iblmulc2nc  38006  ftc1anclem8  38021  ismgmOLD  38171  tsbi1  38454  tsbi2  38455  ac6s6  38493  equid1  39345  ax12fromc15  39351  equid1ALT  39371  dvelimf-o  39375  ax12inda2ALT  39392  ax12inda2  39393  sn-axprlem3  42659  fsuppind  43023  mzpmfp  43179  itgocn  43592  mendbas  43608  mendplusgfval  43609  mendmulrfval  43611  mendsca  43613  mendvscafval  43614  arearect  43643  areaquad  43644  fpwfvss  43839  safesnsupfidom1o  43844  sn1dom  43953  or3or  44450  uneqsn  44452  addcomgi  44882  ax6e2ndeq  44986  2sb5ndVD  45336  2sb5ndALT  45358  sqwvfoura  46656  sqwvfourb  46657  fourierswlem  46658  fouriersw  46659  hspdifhsp  47044  hspmbllem2  47055  hspmbl  47057  et-ltneverrefl  47299  tz6.12-afv  47621  ndmaovcl  47651  tz6.12-afv2  47688  otiunsndisjX  47727  fvmptrab  47740  nltle2tri  47761  fzopredsuc  47772  iccpartiltu  47882  iccpartigtl  47883  iccpartlt  47884  icceuelpartlem  47895  iccpartnel  47898  elsprel  47935  sprssspr  47941  sprsymrelfvlem  47950  prprelprb  47977  prprspr2  47978  fmtnoprmfac1  48028  fmtnoprmfac2  48030  prmdvdsfmtnof1lem2  48048  prminf2  48051  lighneallem4  48073  requad1  48098  requad2  48099  evenprm2  48190  even3prm2  48195  fpprbasnn  48205  stgoldbwt  48252  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  upwlkbprop  48614  pgrpgt2nabl  48842  suppmptcfin  48852  linc1  48901  lindslinindsimp2lem5  48938  1aryenef  49121  2aryenef  49132  reorelicc  49186  rrxsphere  49224  fvconst0ci  49366  fvconstdomi  49367  upfval  49651  reldmprcof1  49856  reldmprcof2  49857  lmdfval  50124  cmdfval  50125  setrec2lem1  50168  setrec2mpt  50172