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  811  ecase3  1032  4cases  1040  pm4.42  1053  ifpid  1076  elimh  1082  3ecase  1476  norass  1538  ax6e  2385  ax12  2425  exdistrf  2449  equvini  2457  ax12vALT  2471  2ax6e  2473  sb1  2480  sb2  2481  sb4a  2482  dfsb1  2483  dfsb2  2495  sbcom3  2508  sbco2  2513  sbco3  2515  sb9  2521  eujustALT  2569  pm2.61ine  3013  ralcom2  3345  eueq2  3666  moeq3  3668  mo2icl  3670  sbc2or  3747  unineq  4239  csb0  4361  sbcel12  4362  sbcne12  4366  sbcel2  4369  csbidm  4384  csbun  4392  csbin  4393  csbdif  4475  ifsb  4490  ifid  4517  ifnot  4529  ifan  4530  ifor  4531  csbif  4534  elimhyp  4542  elimhyp2v  4543  elimhyp3v  4544  elimhyp4v  4545  elimdhyp  4547  keephyp2v  4549  keephyp3v  4550  rmosn  4673  rabsnif  4677  tppreqb  4758  ssunsn2  4780  n0snor2el  4786  preq12nebg  4816  opthprneg  4818  elpreqprlem  4819  dfopif  4823  csbuni  4890  disjord  5084  sbcbr  5150  unisn2  5254  intabs  5291  class2set  5297  dtruALT2  5312  snexALT  5325  dtruALT  5330  axprlem3  5367  axprlem3OLD  5370  snex  5378  exneq  5382  copsexgw  5435  copsexg  5436  snopeqop  5451  csbopab  5500  dfid3  5519  csbxp  5722  csbres  5938  csbima12  6035  soirri  6080  csbrn  6158  dmsnopss  6169  dmsnsnsn  6175  opswap  6184  unixpid  6239  predres  6294  nsuceq0  6399  ordsssuc2  6407  iotassuni  6464  iotaex  6465  csbiota  6482  dffv3  6827  fvrn0  6859  ndmfv  6863  elfv2ex  6874  fveqres  6875  csbfv12  6876  csbfv  6878  dffv2  6926  fvco4i  6932  fvmptss  6950  fvmptex  6952  fvmptss2  6964  fvmptrabfv  6970  f0cli  7040  fvunsn  7122  fconst5  7149  csbriota  7327  riotassuni  7352  oprabidw  7386  csbov123  7399  csbov  7400  fvmptopab  7410  brfvopab  7412  elimdelov  7451  ovif12  7455  ifmpt2v  7457  ndmovcl  7540  ndmovord  7545  elovmpt3imp  7612  difsnexi  7703  ordsuc  7753  ordsucelsuc  7761  1stval  7932  2ndval  7933  1st2val  7958  2nd2val  7959  el2mpocsbcl  8024  bropopvvv  8029  bropfvvvvlem  8030  bropfvvvv  8031  suppimacnv  8113  suppssdm  8116  ressuppss  8122  suppun  8123  extmptsuppeq  8127  funsssuppss  8129  fczsupp0  8132  suppss  8133  suppss2  8139  suppssfv  8141  suppco  8145  mpoxopynvov0  8157  mpoxopoveqd  8160  pwuninel  8214  smofvon2  8285  om0x  8443  mapssfset  8784  brdomg  8890  snfi  8975  sdomirr  9037  domunsn  9050  2pwuninel  9055  unfi  9090  cnvfi  9095  suppeqfsuppbi  9273  fsuppun  9281  funsnfsupp  9286  fipwuni  9320  oicl  9425  oif  9426  wemapso2  9449  card2on  9450  en2lp  9506  ttrclselem1  9625  tctr  9638  r1tr  9679  rankdmr1  9704  r1pw  9748  r1pwALT  9749  rankuni  9766  scottex  9788  cardidm  9862  alephcard  9971  alephnbtwn  9972  cfub  10150  cardcf  10153  cflecard  10154  cfle  10155  cflim2  10164  cfidm  10176  isf32lem9  10262  itunisuc  10320  itunitc1  10321  itunitc  10322  ituniiun  10323  axcc2lem  10337  alephreg  10483  pwcfsdom  10484  cfpwsdom  10485  axunndlem1  10496  axpownd  10502  tskmcl  10742  addcompi  10795  addasspi  10796  mulcompi  10797  mulasspi  10798  distrpi  10799  addnidpi  10802  nlt1pi  10807  addcompq  10851  addcomnq  10852  mulcompq  10853  mulcomnq  10854  adderpq  10857  mulerpq  10858  addassnq  10859  mulassnq  10860  distrnq  10862  genpass  10910  addcompr  10922  mulcompr  10924  distrpr  10929  ltexprlem7  10943  addcomsr  10988  addasssr  10989  mulcomsr  10990  mulasssr  10991  distrsr  10992  uzssz  12763  uzwo  12819  nn01to3  12849  xnn0xaddcl  13144  elixx3g  13268  iooid  13283  elfz2  13424  injresinjlem  13700  injresinj  13701  fleqceilz  13768  modifeq2int  13850  modfzo0difsn  13860  addmodlteq  13863  ltweuz  13878  fzofi  13891  fsuppmapnn0fiubex  13909  hashrabrsn  14289  hashrabsn01  14290  hashrabsn1  14291  elprchashprn2  14313  hashss  14326  hashsn01  14333  hash1snb  14336  hashgt12el  14339  hashgt12el2  14340  hashgt23el  14341  hashfzp1  14348  hashfundm  14359  hash2pwpr  14393  hashge2el2dif  14397  hash3tpde  14410  ffz0iswrd  14458  ccatsymb  14500  swrd00  14562  swrd0  14576  swrdwrdsymb  14580  pfx00  14592  pfx0  14593  repswswrd  14701  0csh0  14710  cshwcl  14715  cshwidxmod  14720  repswcshw  14729  cshw1  14739  s3sndisj  14884  s3iunsndisj  14885  xptrrel  14897  trclfvcotrg  14933  relexpfld  14966  reusq0  15382  modfsummods  15710  dvdsaddre2b  16228  gcdaddmlem  16445  prm23ge5  16737  pcmptcl  16813  prmgaplem5  16977  prmgaplem6  16978  cshwshash  17026  strle1  17079  strfvss  17108  strfvi  17111  setsnid  17129  ressbas  17157  ressbasssg  17158  ressbasssOLD  17161  resseqnbas  17163  ress0  17164  ressress  17168  0rest  17343  firest  17346  topnval  17348  xpsaddlem  17487  xpsvsca  17491  homffval  17606  comfffval  17614  oppchomfval  17630  oppcbas  17634  fullfunc  17825  fthfunc  17826  natfval  17866  fucbas  17880  fuchom  17881  arwval  17960  coafval  17981  xpcbas  18094  xpchomfval  18095  xpccofval  18098  oduval  18204  oduleval  18205  lubfun  18266  glbfun  18279  odujoin  18322  odumeet  18324  ipopos  18452  plusffval  18564  grpidval  18579  gsum0  18602  frmdplusg  18772  frmd0  18778  efmndbas  18789  efmndbasabf  18790  efmndplusg  18798  mgm2nsgrplem2  18837  mgm2nsgrplem3  18838  sgrp2rid2  18844  dfgrp2e  18886  grpinvfval  18901  grpinvfvalALT  18902  grpinvfvi  18905  grpsubfval  18906  grpsubfvalALT  18907  mulgfval  18992  mulgfvalALT  18993  mulgfvi  18996  cntrval  19241  oppgval  19269  oppgplusfval  19270  symgval  19293  snsymgefmndeq  19317  psgnfval  19422  odfval  19454  odfvalALT  19455  oppglsm  19564  efgval  19639  mgpval  20071  mgpplusg  20072  ringidval  20111  opprval  20266  opprmulfval  20267  dvdsrval  20289  invrfval  20317  dvrfval  20330  rrgval  20622  staffval  20766  scaffval  20823  rlmval  21135  rlmsca2  21143  2idlval  21198  nzerooringczr  21427  zrhval  21454  zlmlem  21463  zlmvsca  21468  chrval  21470  evpmss  21533  psgndiflemB  21547  ipffval  21595  thlbas  21643  thlle  21644  thloc  21646  pjfval  21653  dsmmval2  21683  asclfval  21826  psrplusg  21883  psrmulr  21889  psrvscafval  21895  mplval  21936  mplcoe3  21983  evlval  22040  psr1val  22108  vr1val  22114  ply1val  22116  ply1basfvi  22163  ply1plusgfvi  22164  psr1sca2  22173  ply1sca2  22176  ply1ascl  22182  cply1mul  22221  gsummoncoe1  22233  evl1fval  22253  evl1fval1  22256  mamufacex  22321  mavmulsolcl  22476  marrepfval  22485  marepvfval  22490  submafval  22504  mdetfval  22511  mdetfval1  22515  mdetunilem7  22543  mdetunilem8  22544  madufval  22562  minmar1fval  22571  mp2pm2mplem4  22734  toponsspwpw  22847  tgdif0  22917  indislem  22925  resstopn  23111  iocpnfordt  23140  icomnfordt  23141  hmeofval  23683  ussval  24184  nmfval  24513  nghmfval  24647  pcofval  24947  tcphval  25155  ioombl  25503  ibladdlem  25758  itgaddlem1  25761  iblabs  25767  dvbsss  25840  perfdvf  25841  mdegfval  26004  deg1fval  26022  deg1fvi  26027  uc1pval  26082  mon1pval  26084  2irrexpq  26677  lgsqrmodndvds  27301  gausslemma2dlem1a  27313  2lgs  27355  2sqreultblem  27396  2sqreunnltblem  27399  newval  27806  leftval  27814  rightval  27815  lltropt  27827  oldssmade  27832  oldss  27833  lrold  27852  ttglem  28864  axcontlem12  28964  vtxval  28989  iedgval  28990  edgval  29038  usgr1v  29245  nbuhgr  29332  nbumgr  29336  uhgrnbgr0nb  29343  nbgr1vtx  29347  nbgrnself2  29349  nbusgrvtxm1  29368  sizusglecusg  29453  g0wlk0  29640  wlkreslem  29657  lfgrwlkprop  29675  wwlks  29824  wwlksn  29826  wspthsn  29837  iswwlksnon  29842  iswspthsnon  29845  0enwwlksnge1  29853  wwlksnfi  29895  clwwlk  29974  umgrclwwlkge2  29982  clwlkclwwlklem2a4  29988  clwwlkn  30017  clwwlknonmpo  30080  clwwlknon  30081  clwwlk0on0  30083  clwwlknon1le1  30092  1conngr  30185  eupth2lem3lem7  30225  frgr1v  30262  nfrgr2v  30263  1to2vfriswmgr  30270  2wspmdisj  30328  frgrreggt1  30384  frgrreg  30385  frgrregord013  30386  frgrogt3nreg  30388  friendship  30390  avril1  30454  vafval  30594  bafval  30595  smfval  30596  vsfval  30624  bcsiALT  31170  of0r  32671  fracval  33281  fracbas  33282  resvsca  33308  resvlem  33309  cntnevol  34252  signsw0glem  34577  bnj1189  35032  r1wf  35118  fmlafvel  35440  gonan0  35447  satffun  35464  mvtval  35555  mexval  35557  mexval2  35558  mdvval  35559  mrsubfval  35563  mrsubrn  35568  msubfval  35579  elmsubrn  35583  msubrn  35584  mvhfval  35588  mpstval  35590  msrfval  35592  mstaval  35599  mppsval  35627  mthmval  35630  antnestlaw2  35747  dfrdg3  35849  fvsingle  35973  unisnif  35978  funpartfv  36000  fullfunfv  36002  linedegen  36198  bj-ax6e  36723  axc11n11r  36738  bj-ax12v3ALT  36741  bj-sbsb  36892  bj-nfcsym  36954  bj-snex  37090  bj-restsnid  37142  bj-inftyexpitaudisj  37260  bj-inftyexpidisj  37265  finxpreclem4  37449  finxp00  37457  isinf2  37460  wl-nfs1t  37592  matunitlindflem1  37666  itg2addnclem  37721  ibladdnclem  37726  itgaddnclem1  37728  iblabsnc  37734  iblmulc2nc  37735  ftc1anclem8  37750  ismgmOLD  37900  tsbi1  38183  tsbi2  38184  ac6s6  38222  equid1  39008  ax12fromc15  39014  equid1ALT  39034  dvelimf-o  39038  ax12inda2ALT  39055  ax12inda2  39056  sn-axprlem3  42325  fsuppind  42698  mzpmfp  42854  itgocn  43271  mendbas  43287  mendplusgfval  43288  mendmulrfval  43290  mendsca  43292  mendvscafval  43293  arearect  43322  areaquad  43323  fpwfvss  43519  safesnsupfidom1o  43524  sn1dom  43633  or3or  44130  uneqsn  44132  addcomgi  44562  ax6e2ndeq  44666  2sb5ndVD  45016  2sb5ndALT  45038  sqwvfoura  46340  sqwvfourb  46341  fourierswlem  46342  fouriersw  46343  hspdifhsp  46728  hspmbllem2  46739  hspmbl  46741  et-ltneverrefl  46983  tz6.12-afv  47287  ndmaovcl  47317  tz6.12-afv2  47354  otiunsndisjX  47393  fvmptrab  47406  nltle2tri  47427  fzopredsuc  47437  iccpartiltu  47536  iccpartigtl  47537  iccpartlt  47538  icceuelpartlem  47549  iccpartnel  47552  elsprel  47589  sprssspr  47595  sprsymrelfvlem  47604  prprelprb  47631  prprspr2  47632  fmtnoprmfac1  47679  fmtnoprmfac2  47681  prmdvdsfmtnof1lem2  47699  prminf2  47702  lighneallem4  47724  requad1  47736  requad2  47737  evenprm2  47828  even3prm2  47833  fpprbasnn  47843  stgoldbwt  47890  pgnbgreunbgrlem2lem1  48228  pgnbgreunbgrlem2lem2  48229  pgnbgreunbgrlem2lem3  48230  upwlkbprop  48252  pgrpgt2nabl  48480  suppmptcfin  48490  linc1  48540  lindslinindsimp2lem5  48577  1aryenef  48760  2aryenef  48771  reorelicc  48825  rrxsphere  48863  fvconst0ci  49005  fvconstdomi  49006  upfval  49291  reldmprcof1  49496  reldmprcof2  49497  lmdfval  49764  cmdfval  49765  setrec2lem1  49808  setrec2mpt  49812