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  377  pm5.18  380  biass  383  pm2.61ian  808  ecase3  1028  4cases  1037  pm4.42  1050  ifpid  1074  elimh  1081  3ecase  1472  norass  1536  ax6e  2380  ax12  2420  exdistrf  2444  equvini  2452  ax12vALT  2466  2ax6e  2468  sb1  2475  sb2  2476  sb4a  2477  dfsb1  2478  dfsb2  2490  sbcom3  2503  sbco2  2508  sbco3  2510  sb9  2516  eujustALT  2564  pm2.61ine  3023  ralcom2  3371  eueq2  3705  moeq3  3707  mo2icl  3709  sbc2or  3785  unineq  4276  csb0  4406  sbcel12  4407  sbcne12  4411  sbcel2  4414  csbidm  4429  csbun  4437  csbin  4438  ralidmOLD  4514  csbdif  4526  ifsb  4540  ifid  4567  ifnot  4579  ifan  4580  ifor  4581  csbif  4584  elimhyp  4592  elimhyp2v  4593  elimhyp3v  4594  elimhyp4v  4595  elimdhyp  4597  keephyp2v  4599  keephyp3v  4600  rmosn  4722  rabsnif  4726  tppreqb  4807  ssunsn2  4829  n0snor2el  4833  preq12nebg  4862  opthprneg  4864  elpreqprlem  4865  dfopif  4869  csbuni  4939  disjord  5135  sbcbr  5202  unisn2  5311  intabs  5341  class2set  5352  dtruALT2  5367  snexALT  5380  dtruALT  5385  axprlem3  5422  snex  5430  exneq  5434  dtruOLD  5440  copsexgw  5489  copsexg  5490  snopeqop  5505  csbopab  5554  0nelopabOLD  5567  dfid3  5576  csbxp  5774  csbres  5983  csbima12  6077  soirri  6126  csbrn  6201  dmsnopss  6212  dmsnsnsn  6218  opswap  6227  unixpid  6282  predres  6339  nsuceq0  6446  ordsssuc2  6454  iotassuni  6514  iotaex  6515  iotassuniOLD  6521  iotaexOLD  6522  csbiota  6535  dffv3  6886  fvrn0  6920  ndmfv  6925  elfv2ex  6936  fveqres  6937  csbfv12  6938  csbfv  6940  dffv2  6985  fvco4i  6991  fvmptss  7009  fvmptex  7011  fvmptss2  7022  fvmptrabfv  7028  f0cli  7098  fvunsn  7178  fconst5  7208  csbriota  7383  riotassuni  7408  oprabidw  7442  csbov123  7453  csbov  7454  fvmptopab  7465  fvmptopabOLD  7466  brfvopab  7468  elimdelov  7507  ovif12  7510  ndmovcl  7594  ndmovord  7599  elovmpt3imp  7665  difsnexi  7750  ordsuc  7803  ordsucOLD  7804  ordsucelsuc  7812  1stval  7979  2ndval  7980  1st2val  8005  2nd2val  8006  el2mpocsbcl  8073  bropopvvv  8078  bropfvvvvlem  8079  bropfvvvv  8080  suppimacnv  8161  suppssdm  8164  ressuppss  8170  suppun  8171  extmptsuppeq  8175  funsssuppss  8177  fczsupp0  8180  suppss  8181  suppssOLD  8182  suppssov1  8185  suppss2  8187  suppssfv  8189  suppco  8193  mpoxopynvov0  8205  mpoxopoveqd  8208  pwuninel  8262  smofvon2  8358  om0x  8521  mapssfset  8847  brdomg  8954  brdomgOLD  8955  snfi  9046  sdomirr  9116  domunsn  9129  2pwuninel  9134  unfi  9174  cnvfi  9182  snnen2oOLD  9229  suppeqfsuppbi  9379  fsuppun  9384  funsnfsupp  9389  fipwuni  9423  oicl  9526  oif  9527  wemapso2  9550  card2on  9551  en2lp  9603  ttrclselem1  9722  tctr  9737  r1tr  9773  rankdmr1  9798  r1pw  9842  r1pwALT  9843  rankuni  9860  scottex  9882  cardidm  9956  alephcard  10067  alephnbtwn  10068  cfub  10246  cardcf  10249  cflecard  10250  cfle  10251  cflim2  10260  cfidm  10272  isf32lem9  10358  itunisuc  10416  itunitc1  10417  itunitc  10418  ituniiun  10419  axcc2lem  10433  alephreg  10579  pwcfsdom  10580  cfpwsdom  10581  axunndlem1  10592  axpownd  10598  tskmcl  10838  addcompi  10891  addasspi  10892  mulcompi  10893  mulasspi  10894  distrpi  10895  addnidpi  10898  nlt1pi  10903  addcompq  10947  addcomnq  10948  mulcompq  10949  mulcomnq  10950  adderpq  10953  mulerpq  10954  addassnq  10955  mulassnq  10956  distrnq  10958  genpass  11006  addcompr  11018  mulcompr  11020  distrpr  11025  ltexprlem7  11039  addcomsr  11084  addasssr  11085  mulcomsr  11086  mulasssr  11087  distrsr  11088  uzssz  12847  uzwo  12899  nn01to3  12929  xnn0xaddcl  13218  elixx3g  13341  iooid  13356  elfz2  13495  injresinjlem  13756  injresinj  13757  fleqceilz  13823  modifeq2int  13902  modfzo0difsn  13912  addmodlteq  13915  ltweuz  13930  fzofi  13943  fsuppmapnn0fiubex  13961  hashrabrsn  14336  hashrabsn01  14337  hashrabsn1  14338  elprchashprn2  14360  hashss  14373  hashsn01  14380  hash1snb  14383  hashgt12el  14386  hashgt12el2  14387  hashgt23el  14388  hashfzp1  14395  hashfundm  14406  hash2pwpr  14441  hashge2el2dif  14445  ffz0iswrd  14495  ccatsymb  14536  swrd00  14598  swrd0  14612  swrdwrdsymb  14616  pfx00  14628  pfx0  14629  repswswrd  14738  0csh0  14747  cshwcl  14752  cshwidxmod  14757  repswcshw  14766  cshw1  14776  s3sndisj  14918  s3iunsndisj  14919  xptrrel  14931  trclfvcotrg  14967  relexpfld  15000  reusq0  15413  modfsummods  15743  dvdsaddre2b  16254  gcdaddmlem  16469  prm23ge5  16752  pcmptcl  16828  prmgaplem5  16992  prmgaplem6  16993  cshwshash  17042  strle1  17095  strfvss  17124  strfvi  17127  setsnid  17146  setsnidOLD  17147  ressbas  17183  ressbasOLD  17184  ressbasssg  17185  ressbasssOLD  17188  resseqnbas  17190  resslemOLD  17191  ress0  17192  ressress  17197  0rest  17379  firest  17382  topnval  17384  xpsaddlem  17523  xpsvsca  17527  homffval  17638  comfffval  17646  oppchomfval  17662  oppchomfvalOLD  17663  oppcbas  17667  oppcbasOLD  17668  fullfunc  17861  fthfunc  17862  natfval  17901  fucbas  17916  fuchom  17917  fuchomOLD  17918  arwval  17997  coafval  18018  xpcbas  18134  xpchomfval  18135  xpccofval  18138  oduval  18245  oduleval  18246  lubfun  18309  glbfun  18322  odujoin  18365  odumeet  18367  ipopos  18493  plusffval  18571  grpidval  18586  gsum0  18609  frmdplusg  18771  frmd0  18777  efmndbas  18788  efmndbasabf  18789  efmndplusg  18797  mgm2nsgrplem2  18836  mgm2nsgrplem3  18837  sgrp2rid2  18843  dfgrp2e  18884  grpinvfval  18899  grpinvfvalALT  18900  grpinvfvi  18903  grpsubfval  18904  grpsubfvalALT  18905  mulgfval  18988  mulgfvalALT  18989  mulgfvi  18992  cntrval  19224  oppgval  19252  oppgplusfval  19253  symgval  19277  snsymgefmndeq  19303  psgnfval  19409  odfval  19441  odfvalALT  19442  oppglsm  19551  efgval  19626  mgpval  20031  mgpplusg  20032  ringidval  20077  opprval  20226  opprmulfval  20227  dvdsrval  20252  invrfval  20280  dvrfval  20293  staffval  20598  scaffval  20634  rlmval  20958  rlmsca2  20968  2idlval  21007  rrgval  21103  zrhval  21276  zlmlem  21285  zlmlemOLD  21286  zlmvsca  21294  chrval  21296  evpmss  21358  psgndiflemB  21372  ipffval  21420  thlbas  21468  thlbasOLD  21469  thlle  21470  thlleOLD  21471  thloc  21473  pjfval  21480  dsmmval2  21510  asclfval  21652  psrplusg  21719  psrmulr  21722  psrvscafval  21728  mplval  21767  mplcoe3  21812  evlval  21877  psr1val  21929  vr1val  21935  ply1val  21937  ply1basfvi  21983  ply1plusgfvi  21984  psr1sca2  21993  ply1sca2  21996  ply1ascl  22000  cply1mul  22038  gsummoncoe1  22048  evl1fval  22067  evl1fval1  22070  mamufacex  22111  mavmulsolcl  22273  marrepfval  22282  marepvfval  22287  submafval  22301  mdetfval  22308  mdetfval1  22312  mdetunilem7  22340  mdetunilem8  22341  madufval  22359  minmar1fval  22368  mp2pm2mplem4  22531  toponsspwpw  22644  tgdif0  22715  indislem  22723  resstopn  22910  iocpnfordt  22939  icomnfordt  22940  hmeofval  23482  ussval  23984  nmfval  24317  nghmfval  24459  pcofval  24757  tcphval  24966  ioombl  25314  ibladdlem  25569  itgaddlem1  25572  iblabs  25578  dvbsss  25651  perfdvf  25652  mdegfval  25815  deg1fval  25833  deg1fvi  25838  uc1pval  25892  mon1pval  25894  2irrexpq  26475  lgsqrmodndvds  27092  gausslemma2dlem1a  27104  2lgs  27146  2sqreultblem  27187  2sqreunnltblem  27190  newval  27587  leftval  27595  rightval  27596  lltropt  27604  oldssmade  27609  lrold  27628  ttglem  28395  ttglemOLD  28396  axcontlem12  28500  vtxval  28527  iedgval  28528  edgval  28576  usgr1v  28780  nbuhgr  28867  nbumgr  28871  uhgrnbgr0nb  28878  nbgr1vtx  28882  nbgrnself2  28884  nbusgrvtxm1  28903  sizusglecusg  28987  g0wlk0  29176  wlkreslem  29193  lfgrwlkprop  29211  wwlks  29356  wwlksn  29358  wspthsn  29369  iswwlksnon  29374  iswspthsnon  29377  0enwwlksnge1  29385  wwlksnfi  29427  clwwlk  29503  umgrclwwlkge2  29511  clwlkclwwlklem2a4  29517  clwwlkn  29546  clwwlknonmpo  29609  clwwlknon  29610  clwwlk0on0  29612  clwwlknon1le1  29621  1conngr  29714  eupth2lem3lem7  29754  frgr1v  29791  nfrgr2v  29792  1to2vfriswmgr  29799  2wspmdisj  29857  frgrreggt1  29913  frgrreg  29914  frgrregord013  29915  frgrogt3nreg  29917  friendship  29919  avril1  29983  vafval  30123  bafval  30124  smfval  30125  vsfval  30153  bcsiALT  30699  resvsca  32714  resvlem  32715  resvlemOLD  32716  cntnevol  33524  signsw0glem  33862  bnj1189  34318  fmlafvel  34674  gonan0  34681  satffun  34698  mvtval  34789  mexval  34791  mexval2  34792  mdvval  34793  mrsubfval  34797  mrsubrn  34802  msubfval  34813  elmsubrn  34817  msubrn  34818  mvhfval  34822  mpstval  34824  msrfval  34826  mstaval  34833  mppsval  34861  mthmval  34864  dfrdg3  35072  fvsingle  35196  unisnif  35201  funpartfv  35221  fullfunfv  35223  linedegen  35419  bj-ax6e  35848  axc11n11r  35864  bj-ax12v3ALT  35867  bj-sbsb  36018  bj-nfcsym  36082  bj-snex  36219  bj-restsnid  36271  bj-inftyexpitaudisj  36389  bj-inftyexpidisj  36394  finxpreclem4  36578  finxp00  36586  isinf2  36589  wl-nfs1t  36709  matunitlindflem1  36787  itg2addnclem  36842  ibladdnclem  36847  itgaddnclem1  36849  iblabsnc  36855  iblmulc2nc  36856  ftc1anclem8  36871  ismgmOLD  37021  tsbi1  37304  tsbi2  37305  ac6s6  37343  equid1  38072  ax12fromc15  38078  equid1ALT  38098  dvelimf-o  38102  ax12inda2ALT  38119  ax12inda2  38120  sn-axprlem3  41340  fsuppind  41464  mzpmfp  41787  itgocn  42208  mendbas  42228  mendplusgfval  42229  mendmulrfval  42231  mendsca  42233  mendvscafval  42234  arearect  42266  areaquad  42267  fpwfvss  42465  safesnsupfidom1o  42470  sn1dom  42579  or3or  43076  uneqsn  43078  addcomgi  43517  ax6e2ndeq  43622  2sb5ndVD  43973  2sb5ndALT  43995  sqwvfoura  45242  sqwvfourb  45243  fourierswlem  45244  fouriersw  45245  hspdifhsp  45630  hspmbllem2  45641  hspmbl  45643  et-ltneverrefl  45885  tz6.12-afv  46179  ndmaovcl  46209  tz6.12-afv2  46246  otiunsndisjX  46285  fvmptrab  46298  nltle2tri  46319  fzopredsuc  46329  iccpartiltu  46388  iccpartigtl  46389  iccpartlt  46390  icceuelpartlem  46401  iccpartnel  46404  elsprel  46441  sprssspr  46447  sprsymrelfvlem  46456  prprelprb  46483  prprspr2  46484  fmtnoprmfac1  46531  fmtnoprmfac2  46533  prmdvdsfmtnof1lem2  46551  prminf2  46554  lighneallem4  46576  requad1  46588  requad2  46589  evenprm2  46680  even3prm2  46685  fpprbasnn  46695  stgoldbwt  46742  upwlkbprop  46814  nzerooringczr  47058  pgrpgt2nabl  47130  suppmptcfin  47143  linc1  47193  lindslinindsimp2lem5  47230  1aryenef  47418  2aryenef  47429  reorelicc  47483  rrxsphere  47521  fvconst0ci  47612  fvconstdomi  47613  setrec2lem1  47825  setrec2mpt  47829