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  1537  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  3008  ralcom2  3348  eueq2  3678  moeq3  3680  mo2icl  3682  sbc2or  3759  unineq  4247  csb0  4369  sbcel12  4370  sbcne12  4374  sbcel2  4377  csbidm  4392  csbun  4400  csbin  4401  csbdif  4483  ifsb  4498  ifid  4525  ifnot  4537  ifan  4538  ifor  4539  csbif  4542  elimhyp  4550  elimhyp2v  4551  elimhyp3v  4552  elimhyp4v  4553  elimdhyp  4555  keephyp2v  4557  keephyp3v  4558  rmosn  4679  rabsnif  4683  tppreqb  4765  ssunsn2  4787  n0snor2el  4793  preq12nebg  4823  opthprneg  4825  elpreqprlem  4826  dfopif  4830  csbuni  4896  disjord  5091  sbcbr  5157  unisn2  5262  intabs  5299  class2set  5305  dtruALT2  5320  snexALT  5333  dtruALT  5338  axprlem3  5375  axprlem3OLD  5378  snex  5386  exneq  5390  dtruOLD  5396  copsexgw  5445  copsexg  5446  snopeqop  5461  csbopab  5510  dfid3  5529  csbxp  5730  csbres  5942  csbima12  6039  soirri  6087  csbrn  6164  dmsnopss  6175  dmsnsnsn  6181  opswap  6190  unixpid  6245  predres  6300  nsuceq0  6405  ordsssuc2  6413  iotassuni  6471  iotaex  6472  iotassuniOLD  6478  iotaexOLD  6479  csbiota  6492  dffv3  6836  fvrn0  6870  ndmfv  6875  elfv2ex  6886  fveqres  6887  csbfv12  6888  csbfv  6890  dffv2  6938  fvco4i  6944  fvmptss  6962  fvmptex  6964  fvmptss2  6976  fvmptrabfv  6982  f0cli  7052  fvunsn  7135  fconst5  7162  csbriota  7341  riotassuni  7366  oprabidw  7400  csbov123  7413  csbov  7414  fvmptopab  7424  brfvopab  7426  elimdelov  7465  ovif12  7469  ifmpt2v  7471  ndmovcl  7554  ndmovord  7559  elovmpt3imp  7626  difsnexi  7717  ordsuc  7768  ordsucOLD  7769  ordsucelsuc  7777  1stval  7949  2ndval  7950  1st2val  7975  2nd2val  7976  el2mpocsbcl  8041  bropopvvv  8046  bropfvvvvlem  8047  bropfvvvv  8048  suppimacnv  8130  suppssdm  8133  ressuppss  8139  suppun  8140  extmptsuppeq  8144  funsssuppss  8146  fczsupp0  8149  suppss  8150  suppss2  8156  suppssfv  8158  suppco  8162  mpoxopynvov0  8174  mpoxopoveqd  8177  pwuninel  8231  smofvon2  8302  om0x  8460  mapssfset  8801  brdomg  8907  snfi  8991  snfiOLD  8992  sdomirr  9055  domunsn  9068  2pwuninel  9073  unfi  9112  cnvfi  9117  suppeqfsuppbi  9306  fsuppun  9314  funsnfsupp  9319  fipwuni  9353  oicl  9458  oif  9459  wemapso2  9482  card2on  9483  en2lp  9535  ttrclselem1  9654  tctr  9669  r1tr  9705  rankdmr1  9730  r1pw  9774  r1pwALT  9775  rankuni  9792  scottex  9814  cardidm  9888  alephcard  9999  alephnbtwn  10000  cfub  10178  cardcf  10181  cflecard  10182  cfle  10183  cflim2  10192  cfidm  10204  isf32lem9  10290  itunisuc  10348  itunitc1  10349  itunitc  10350  ituniiun  10351  axcc2lem  10365  alephreg  10511  pwcfsdom  10512  cfpwsdom  10513  axunndlem1  10524  axpownd  10530  tskmcl  10770  addcompi  10823  addasspi  10824  mulcompi  10825  mulasspi  10826  distrpi  10827  addnidpi  10830  nlt1pi  10835  addcompq  10879  addcomnq  10880  mulcompq  10881  mulcomnq  10882  adderpq  10885  mulerpq  10886  addassnq  10887  mulassnq  10888  distrnq  10890  genpass  10938  addcompr  10950  mulcompr  10952  distrpr  10957  ltexprlem7  10971  addcomsr  11016  addasssr  11017  mulcomsr  11018  mulasssr  11019  distrsr  11020  uzssz  12790  uzwo  12846  nn01to3  12876  xnn0xaddcl  13171  elixx3g  13295  iooid  13310  elfz2  13451  injresinjlem  13724  injresinj  13725  fleqceilz  13792  modifeq2int  13874  modfzo0difsn  13884  addmodlteq  13887  ltweuz  13902  fzofi  13915  fsuppmapnn0fiubex  13933  hashrabrsn  14313  hashrabsn01  14314  hashrabsn1  14315  elprchashprn2  14337  hashss  14350  hashsn01  14357  hash1snb  14360  hashgt12el  14363  hashgt12el2  14364  hashgt23el  14365  hashfzp1  14372  hashfundm  14383  hash2pwpr  14417  hashge2el2dif  14421  hash3tpde  14434  ffz0iswrd  14482  ccatsymb  14523  swrd00  14585  swrd0  14599  swrdwrdsymb  14603  pfx00  14615  pfx0  14616  repswswrd  14725  0csh0  14734  cshwcl  14739  cshwidxmod  14744  repswcshw  14753  cshw1  14763  s3sndisj  14909  s3iunsndisj  14910  xptrrel  14922  trclfvcotrg  14958  relexpfld  14991  reusq0  15407  modfsummods  15735  dvdsaddre2b  16253  gcdaddmlem  16470  prm23ge5  16762  pcmptcl  16838  prmgaplem5  17002  prmgaplem6  17003  cshwshash  17051  strle1  17104  strfvss  17133  strfvi  17136  setsnid  17154  ressbas  17182  ressbasssg  17183  ressbasssOLD  17186  resseqnbas  17188  ress0  17189  ressress  17193  0rest  17368  firest  17371  topnval  17373  xpsaddlem  17512  xpsvsca  17516  homffval  17631  comfffval  17639  oppchomfval  17655  oppcbas  17659  fullfunc  17850  fthfunc  17851  natfval  17891  fucbas  17905  fuchom  17906  arwval  17985  coafval  18006  xpcbas  18119  xpchomfval  18120  xpccofval  18123  oduval  18229  oduleval  18230  lubfun  18291  glbfun  18304  odujoin  18347  odumeet  18349  ipopos  18477  plusffval  18555  grpidval  18570  gsum0  18593  frmdplusg  18763  frmd0  18769  efmndbas  18780  efmndbasabf  18781  efmndplusg  18789  mgm2nsgrplem2  18828  mgm2nsgrplem3  18829  sgrp2rid2  18835  dfgrp2e  18877  grpinvfval  18892  grpinvfvalALT  18893  grpinvfvi  18896  grpsubfval  18897  grpsubfvalALT  18898  mulgfval  18983  mulgfvalALT  18984  mulgfvi  18987  cntrval  19233  oppgval  19261  oppgplusfval  19262  symgval  19285  snsymgefmndeq  19309  psgnfval  19414  odfval  19446  odfvalALT  19447  oppglsm  19556  efgval  19631  mgpval  20063  mgpplusg  20064  ringidval  20103  opprval  20258  opprmulfval  20259  dvdsrval  20281  invrfval  20309  dvrfval  20322  rrgval  20617  staffval  20761  scaffval  20818  rlmval  21130  rlmsca2  21138  2idlval  21193  nzerooringczr  21422  zrhval  21449  zlmlem  21458  zlmvsca  21463  chrval  21465  evpmss  21528  psgndiflemB  21542  ipffval  21590  thlbas  21638  thlle  21639  thloc  21641  pjfval  21648  dsmmval2  21678  asclfval  21821  psrplusg  21878  psrmulr  21884  psrvscafval  21890  mplval  21931  mplcoe3  21978  evlval  22035  psr1val  22103  vr1val  22109  ply1val  22111  ply1basfvi  22158  ply1plusgfvi  22159  psr1sca2  22168  ply1sca2  22171  ply1ascl  22177  cply1mul  22216  gsummoncoe1  22228  evl1fval  22248  evl1fval1  22251  mamufacex  22316  mavmulsolcl  22471  marrepfval  22480  marepvfval  22485  submafval  22499  mdetfval  22506  mdetfval1  22510  mdetunilem7  22538  mdetunilem8  22539  madufval  22557  minmar1fval  22566  mp2pm2mplem4  22729  toponsspwpw  22842  tgdif0  22912  indislem  22920  resstopn  23106  iocpnfordt  23135  icomnfordt  23136  hmeofval  23678  ussval  24180  nmfval  24509  nghmfval  24643  pcofval  24943  tcphval  25151  ioombl  25499  ibladdlem  25754  itgaddlem1  25757  iblabs  25763  dvbsss  25836  perfdvf  25837  mdegfval  26000  deg1fval  26018  deg1fvi  26023  uc1pval  26078  mon1pval  26080  2irrexpq  26673  lgsqrmodndvds  27297  gausslemma2dlem1a  27309  2lgs  27351  2sqreultblem  27392  2sqreunnltblem  27395  newval  27800  leftval  27808  rightval  27809  lltropt  27821  oldssmade  27826  oldss  27827  lrold  27846  ttglem  28856  axcontlem12  28955  vtxval  28980  iedgval  28981  edgval  29029  usgr1v  29236  nbuhgr  29323  nbumgr  29327  uhgrnbgr0nb  29334  nbgr1vtx  29338  nbgrnself2  29340  nbusgrvtxm1  29359  sizusglecusg  29444  g0wlk0  29631  wlkreslem  29648  lfgrwlkprop  29666  wwlks  29815  wwlksn  29817  wspthsn  29828  iswwlksnon  29833  iswspthsnon  29836  0enwwlksnge1  29844  wwlksnfi  29886  clwwlk  29962  umgrclwwlkge2  29970  clwlkclwwlklem2a4  29976  clwwlkn  30005  clwwlknonmpo  30068  clwwlknon  30069  clwwlk0on0  30071  clwwlknon1le1  30080  1conngr  30173  eupth2lem3lem7  30213  frgr1v  30250  nfrgr2v  30251  1to2vfriswmgr  30258  2wspmdisj  30316  frgrreggt1  30372  frgrreg  30373  frgrregord013  30374  frgrogt3nreg  30376  friendship  30378  avril1  30442  vafval  30582  bafval  30583  smfval  30584  vsfval  30612  bcsiALT  31158  of0r  32652  fracval  33270  fracbas  33271  resvsca  33297  resvlem  33298  cntnevol  34211  signsw0glem  34537  bnj1189  34992  fmlafvel  35365  gonan0  35372  satffun  35389  mvtval  35480  mexval  35482  mexval2  35483  mdvval  35484  mrsubfval  35488  mrsubrn  35493  msubfval  35504  elmsubrn  35508  msubrn  35509  mvhfval  35513  mpstval  35515  msrfval  35517  mstaval  35524  mppsval  35552  mthmval  35555  antnestlaw2  35672  dfrdg3  35777  fvsingle  35901  unisnif  35906  funpartfv  35926  fullfunfv  35928  linedegen  36124  bj-ax6e  36649  axc11n11r  36664  bj-ax12v3ALT  36667  bj-sbsb  36818  bj-nfcsym  36880  bj-snex  37016  bj-restsnid  37068  bj-inftyexpitaudisj  37186  bj-inftyexpidisj  37191  finxpreclem4  37375  finxp00  37383  isinf2  37386  wl-nfs1t  37518  matunitlindflem1  37603  itg2addnclem  37658  ibladdnclem  37663  itgaddnclem1  37665  iblabsnc  37671  iblmulc2nc  37672  ftc1anclem8  37687  ismgmOLD  37837  tsbi1  38120  tsbi2  38121  ac6s6  38159  equid1  38885  ax12fromc15  38891  equid1ALT  38911  dvelimf-o  38915  ax12inda2ALT  38932  ax12inda2  38933  sn-axprlem3  42198  fsuppind  42571  mzpmfp  42728  itgocn  43146  mendbas  43162  mendplusgfval  43163  mendmulrfval  43165  mendsca  43167  mendvscafval  43168  arearect  43197  areaquad  43198  fpwfvss  43394  safesnsupfidom1o  43399  sn1dom  43508  or3or  44005  uneqsn  44007  addcomgi  44438  ax6e2ndeq  44542  2sb5ndVD  44892  2sb5ndALT  44914  sqwvfoura  46219  sqwvfourb  46220  fourierswlem  46221  fouriersw  46222  hspdifhsp  46607  hspmbllem2  46618  hspmbl  46620  et-ltneverrefl  46862  tz6.12-afv  47167  ndmaovcl  47197  tz6.12-afv2  47234  otiunsndisjX  47273  fvmptrab  47286  nltle2tri  47307  fzopredsuc  47317  iccpartiltu  47416  iccpartigtl  47417  iccpartlt  47418  icceuelpartlem  47429  iccpartnel  47432  elsprel  47469  sprssspr  47475  sprsymrelfvlem  47484  prprelprb  47511  prprspr2  47512  fmtnoprmfac1  47559  fmtnoprmfac2  47561  prmdvdsfmtnof1lem2  47579  prminf2  47582  lighneallem4  47604  requad1  47616  requad2  47617  evenprm2  47708  even3prm2  47713  fpprbasnn  47723  stgoldbwt  47770  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  upwlkbprop  48119  pgrpgt2nabl  48347  suppmptcfin  48357  linc1  48407  lindslinindsimp2lem5  48444  1aryenef  48627  2aryenef  48638  reorelicc  48692  rrxsphere  48730  fvconst0ci  48872  fvconstdomi  48873  upfval  49158  reldmprcof1  49363  reldmprcof2  49364  lmdfval  49631  cmdfval  49632  setrec2lem1  49675  setrec2mpt  49679