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  1041  pm4.42  1054  ifpid  1077  elimh  1083  3ecase  1474  norass  1534  ax6e  2391  ax12  2431  exdistrf  2455  equvini  2463  ax12vALT  2477  2ax6e  2479  sb1  2486  sb2  2487  sb4a  2488  dfsb1  2489  dfsb2  2501  sbcom3  2514  sbco2  2519  sbco3  2521  sb9  2527  eujustALT  2575  pm2.61ine  3031  ralcom2  3385  eueq2  3732  moeq3  3734  mo2icl  3736  sbc2or  3813  unineq  4307  csb0  4433  sbcel12  4434  sbcne12  4438  sbcel2  4441  csbidm  4456  csbun  4464  csbin  4465  csbdif  4547  ifsb  4561  ifid  4588  ifnot  4600  ifan  4601  ifor  4602  csbif  4605  elimhyp  4613  elimhyp2v  4614  elimhyp3v  4615  elimhyp4v  4616  elimdhyp  4618  keephyp2v  4620  keephyp3v  4621  rmosn  4744  rabsnif  4748  tppreqb  4830  ssunsn2  4852  n0snor2el  4858  preq12nebg  4887  opthprneg  4889  elpreqprlem  4890  dfopif  4894  csbuni  4960  disjord  5155  sbcbr  5221  unisn2  5330  intabs  5367  class2set  5373  dtruALT2  5388  snexALT  5401  dtruALT  5406  axprlem3  5443  snex  5451  exneq  5455  dtruOLD  5461  copsexgw  5510  copsexg  5511  snopeqop  5525  csbopab  5574  0nelopabOLD  5587  dfid3  5596  csbxp  5799  csbres  6012  csbima12  6108  soirri  6158  csbrn  6234  dmsnopss  6245  dmsnsnsn  6251  opswap  6260  unixpid  6315  predres  6371  nsuceq0  6478  ordsssuc2  6486  iotassuni  6545  iotaex  6546  iotassuniOLD  6552  iotaexOLD  6553  csbiota  6566  dffv3  6916  fvrn0  6950  ndmfv  6955  elfv2ex  6966  fveqres  6967  csbfv12  6968  csbfv  6970  dffv2  7017  fvco4i  7023  fvmptss  7041  fvmptex  7043  fvmptss2  7055  fvmptrabfv  7061  f0cli  7132  fvunsn  7213  fconst5  7243  csbriota  7420  riotassuni  7445  oprabidw  7479  csbov123  7492  csbov  7493  fvmptopab  7504  fvmptopabOLD  7505  brfvopab  7507  elimdelov  7546  ovif12  7550  ndmovcl  7635  ndmovord  7640  elovmpt3imp  7707  difsnexi  7796  ordsuc  7849  ordsucOLD  7850  ordsucelsuc  7858  1stval  8032  2ndval  8033  1st2val  8058  2nd2val  8059  el2mpocsbcl  8126  bropopvvv  8131  bropfvvvvlem  8132  bropfvvvv  8133  suppimacnv  8215  suppssdm  8218  ressuppss  8224  suppun  8225  extmptsuppeq  8229  funsssuppss  8231  fczsupp0  8234  suppss  8235  suppss2  8241  suppssfv  8243  suppco  8247  mpoxopynvov0  8259  mpoxopoveqd  8262  pwuninel  8316  smofvon2  8412  om0x  8575  mapssfset  8909  brdomg  9016  brdomgOLD  9017  snfi  9109  snfiOLD  9110  sdomirr  9180  domunsn  9193  2pwuninel  9198  unfi  9238  cnvfi  9243  snnen2oOLD  9290  suppeqfsuppbi  9448  fsuppun  9456  funsnfsupp  9461  fipwuni  9495  oicl  9598  oif  9599  wemapso2  9622  card2on  9623  en2lp  9675  ttrclselem1  9794  tctr  9809  r1tr  9845  rankdmr1  9870  r1pw  9914  r1pwALT  9915  rankuni  9932  scottex  9954  cardidm  10028  alephcard  10139  alephnbtwn  10140  cfub  10318  cardcf  10321  cflecard  10322  cfle  10323  cflim2  10332  cfidm  10344  isf32lem9  10430  itunisuc  10488  itunitc1  10489  itunitc  10490  ituniiun  10491  axcc2lem  10505  alephreg  10651  pwcfsdom  10652  cfpwsdom  10653  axunndlem1  10664  axpownd  10670  tskmcl  10910  addcompi  10963  addasspi  10964  mulcompi  10965  mulasspi  10966  distrpi  10967  addnidpi  10970  nlt1pi  10975  addcompq  11019  addcomnq  11020  mulcompq  11021  mulcomnq  11022  adderpq  11025  mulerpq  11026  addassnq  11027  mulassnq  11028  distrnq  11030  genpass  11078  addcompr  11090  mulcompr  11092  distrpr  11097  ltexprlem7  11111  addcomsr  11156  addasssr  11157  mulcomsr  11158  mulasssr  11159  distrsr  11160  uzssz  12924  uzwo  12976  nn01to3  13006  xnn0xaddcl  13297  elixx3g  13420  iooid  13435  elfz2  13574  injresinjlem  13837  injresinj  13838  fleqceilz  13905  modifeq2int  13984  modfzo0difsn  13994  addmodlteq  13997  ltweuz  14012  fzofi  14025  fsuppmapnn0fiubex  14043  hashrabrsn  14421  hashrabsn01  14422  hashrabsn1  14423  elprchashprn2  14445  hashss  14458  hashsn01  14465  hash1snb  14468  hashgt12el  14471  hashgt12el2  14472  hashgt23el  14473  hashfzp1  14480  hashfundm  14491  hash2pwpr  14525  hashge2el2dif  14529  hash3tpde  14542  ffz0iswrd  14589  ccatsymb  14630  swrd00  14692  swrd0  14706  swrdwrdsymb  14710  pfx00  14722  pfx0  14723  repswswrd  14832  0csh0  14841  cshwcl  14846  cshwidxmod  14851  repswcshw  14860  cshw1  14870  s3sndisj  15016  s3iunsndisj  15017  xptrrel  15029  trclfvcotrg  15065  relexpfld  15098  reusq0  15511  modfsummods  15841  dvdsaddre2b  16355  gcdaddmlem  16570  prm23ge5  16862  pcmptcl  16938  prmgaplem5  17102  prmgaplem6  17103  cshwshash  17152  strle1  17205  strfvss  17234  strfvi  17237  setsnid  17256  setsnidOLD  17257  ressbas  17293  ressbasOLD  17294  ressbasssg  17295  ressbasssOLD  17298  resseqnbas  17300  resslemOLD  17301  ress0  17302  ressress  17307  0rest  17489  firest  17492  topnval  17494  xpsaddlem  17633  xpsvsca  17637  homffval  17748  comfffval  17756  oppchomfval  17772  oppchomfvalOLD  17773  oppcbas  17777  oppcbasOLD  17778  fullfunc  17973  fthfunc  17974  natfval  18014  fucbas  18029  fuchom  18030  fuchomOLD  18031  arwval  18110  coafval  18131  xpcbas  18247  xpchomfval  18248  xpccofval  18251  oduval  18358  oduleval  18359  lubfun  18422  glbfun  18435  odujoin  18478  odumeet  18480  ipopos  18606  plusffval  18684  grpidval  18699  gsum0  18722  frmdplusg  18889  frmd0  18895  efmndbas  18906  efmndbasabf  18907  efmndplusg  18915  mgm2nsgrplem2  18954  mgm2nsgrplem3  18955  sgrp2rid2  18961  dfgrp2e  19003  grpinvfval  19018  grpinvfvalALT  19019  grpinvfvi  19022  grpsubfval  19023  grpsubfvalALT  19024  mulgfval  19109  mulgfvalALT  19110  mulgfvi  19113  cntrval  19359  oppgval  19387  oppgplusfval  19388  symgval  19412  snsymgefmndeq  19436  psgnfval  19542  odfval  19574  odfvalALT  19575  oppglsm  19684  efgval  19759  mgpval  20164  mgpplusg  20165  ringidval  20210  opprval  20361  opprmulfval  20362  dvdsrval  20387  invrfval  20415  dvrfval  20428  rrgval  20719  staffval  20864  scaffval  20900  rlmval  21221  rlmsca2  21229  2idlval  21284  nzerooringczr  21514  zrhval  21541  zlmlem  21550  zlmlemOLD  21551  zlmvsca  21559  chrval  21561  evpmss  21627  psgndiflemB  21641  ipffval  21689  thlbas  21737  thlbasOLD  21738  thlle  21739  thlleOLD  21740  thloc  21742  pjfval  21749  dsmmval2  21779  asclfval  21922  psrplusg  21979  psrmulr  21985  psrvscafval  21991  mplval  22032  mplcoe3  22079  evlval  22142  psr1val  22208  vr1val  22214  ply1val  22216  ply1basfvi  22263  ply1plusgfvi  22264  psr1sca2  22273  ply1sca2  22276  ply1ascl  22282  cply1mul  22321  gsummoncoe1  22333  evl1fval  22353  evl1fval1  22356  mamufacex  22421  mavmulsolcl  22578  marrepfval  22587  marepvfval  22592  submafval  22606  mdetfval  22613  mdetfval1  22617  mdetunilem7  22645  mdetunilem8  22646  madufval  22664  minmar1fval  22673  mp2pm2mplem4  22836  toponsspwpw  22949  tgdif0  23020  indislem  23028  resstopn  23215  iocpnfordt  23244  icomnfordt  23245  hmeofval  23787  ussval  24289  nmfval  24622  nghmfval  24764  pcofval  25062  tcphval  25271  ioombl  25619  ibladdlem  25875  itgaddlem1  25878  iblabs  25884  dvbsss  25957  perfdvf  25958  mdegfval  26121  deg1fval  26139  deg1fvi  26144  uc1pval  26199  mon1pval  26201  2irrexpq  26791  lgsqrmodndvds  27415  gausslemma2dlem1a  27427  2lgs  27469  2sqreultblem  27510  2sqreunnltblem  27513  newval  27912  leftval  27920  rightval  27921  lltropt  27929  oldssmade  27934  lrold  27953  ttglem  28903  ttglemOLD  28904  axcontlem12  29008  vtxval  29035  iedgval  29036  edgval  29084  usgr1v  29291  nbuhgr  29378  nbumgr  29382  uhgrnbgr0nb  29389  nbgr1vtx  29393  nbgrnself2  29395  nbusgrvtxm1  29414  sizusglecusg  29499  g0wlk0  29688  wlkreslem  29705  lfgrwlkprop  29723  wwlks  29868  wwlksn  29870  wspthsn  29881  iswwlksnon  29886  iswspthsnon  29889  0enwwlksnge1  29897  wwlksnfi  29939  clwwlk  30015  umgrclwwlkge2  30023  clwlkclwwlklem2a4  30029  clwwlkn  30058  clwwlknonmpo  30121  clwwlknon  30122  clwwlk0on0  30124  clwwlknon1le1  30133  1conngr  30226  eupth2lem3lem7  30266  frgr1v  30303  nfrgr2v  30304  1to2vfriswmgr  30311  2wspmdisj  30369  frgrreggt1  30425  frgrreg  30426  frgrregord013  30427  frgrogt3nreg  30429  friendship  30431  avril1  30495  vafval  30635  bafval  30636  smfval  30637  vsfval  30665  bcsiALT  31211  of0r  32696  fracval  33271  fracbas  33272  resvsca  33321  resvlem  33322  resvlemOLD  33323  cntnevol  34192  signsw0glem  34530  bnj1189  34985  fmlafvel  35353  gonan0  35360  satffun  35377  mvtval  35468  mexval  35470  mexval2  35471  mdvval  35472  mrsubfval  35476  mrsubrn  35481  msubfval  35492  elmsubrn  35496  msubrn  35497  mvhfval  35501  mpstval  35503  msrfval  35505  mstaval  35512  mppsval  35540  mthmval  35543  dfrdg3  35760  fvsingle  35884  unisnif  35889  funpartfv  35909  fullfunfv  35911  linedegen  36107  bj-ax6e  36634  axc11n11r  36649  bj-ax12v3ALT  36652  bj-sbsb  36803  bj-nfcsym  36865  bj-snex  37001  bj-restsnid  37053  bj-inftyexpitaudisj  37171  bj-inftyexpidisj  37176  finxpreclem4  37360  finxp00  37368  isinf2  37371  wl-nfs1t  37491  matunitlindflem1  37576  itg2addnclem  37631  ibladdnclem  37636  itgaddnclem1  37638  iblabsnc  37644  iblmulc2nc  37645  ftc1anclem8  37660  ismgmOLD  37810  tsbi1  38093  tsbi2  38094  ac6s6  38132  equid1  38855  ax12fromc15  38861  equid1ALT  38881  dvelimf-o  38885  ax12inda2ALT  38902  ax12inda2  38903  sn-axprlem3  42210  fsuppind  42545  mzpmfp  42703  itgocn  43121  mendbas  43141  mendplusgfval  43142  mendmulrfval  43144  mendsca  43146  mendvscafval  43147  arearect  43176  areaquad  43177  fpwfvss  43374  safesnsupfidom1o  43379  sn1dom  43488  or3or  43985  uneqsn  43987  addcomgi  44425  ax6e2ndeq  44530  2sb5ndVD  44881  2sb5ndALT  44903  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  hspdifhsp  46537  hspmbllem2  46548  hspmbl  46550  et-ltneverrefl  46792  tz6.12-afv  47088  ndmaovcl  47118  tz6.12-afv2  47155  otiunsndisjX  47194  fvmptrab  47207  nltle2tri  47228  fzopredsuc  47238  iccpartiltu  47296  iccpartigtl  47297  iccpartlt  47298  icceuelpartlem  47309  iccpartnel  47312  elsprel  47349  sprssspr  47355  sprsymrelfvlem  47364  prprelprb  47391  prprspr2  47392  fmtnoprmfac1  47439  fmtnoprmfac2  47441  prmdvdsfmtnof1lem2  47459  prminf2  47462  lighneallem4  47484  requad1  47496  requad2  47497  evenprm2  47588  even3prm2  47593  fpprbasnn  47603  stgoldbwt  47650  uspgrimprop  47757  upwlkbprop  47861  pgrpgt2nabl  48091  suppmptcfin  48104  linc1  48154  lindslinindsimp2lem5  48191  1aryenef  48379  2aryenef  48390  reorelicc  48444  rrxsphere  48482  fvconst0ci  48572  fvconstdomi  48573  setrec2lem1  48785  setrec2mpt  48789