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  1032  4cases  1040  pm4.42  1053  ifpid  1076  elimh  1082  3ecase  1473  norass  1533  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  3022  ralcom2  3374  eueq2  3718  moeq3  3720  mo2icl  3722  sbc2or  3799  unineq  4293  csb0  4415  sbcel12  4416  sbcne12  4420  sbcel2  4423  csbidm  4438  csbun  4446  csbin  4447  csbdif  4529  ifsb  4543  ifid  4570  ifnot  4582  ifan  4583  ifor  4584  csbif  4587  elimhyp  4595  elimhyp2v  4596  elimhyp3v  4597  elimhyp4v  4598  elimdhyp  4600  keephyp2v  4602  keephyp3v  4603  rmosn  4723  rabsnif  4727  tppreqb  4809  ssunsn2  4831  n0snor2el  4837  preq12nebg  4867  opthprneg  4869  elpreqprlem  4870  dfopif  4874  csbuni  4940  disjord  5136  sbcbr  5202  unisn2  5317  intabs  5354  class2set  5360  dtruALT2  5375  snexALT  5388  dtruALT  5393  axprlem3  5430  axprlem3OLD  5433  snex  5441  exneq  5445  dtruOLD  5451  copsexgw  5500  copsexg  5501  snopeqop  5515  csbopab  5564  dfid3  5585  csbxp  5787  csbres  6002  csbima12  6098  soirri  6148  csbrn  6224  dmsnopss  6235  dmsnsnsn  6241  opswap  6250  unixpid  6305  predres  6361  nsuceq0  6468  ordsssuc2  6476  iotassuni  6534  iotaex  6535  iotassuniOLD  6541  iotaexOLD  6542  csbiota  6555  dffv3  6902  fvrn0  6936  ndmfv  6941  elfv2ex  6952  fveqres  6953  csbfv12  6954  csbfv  6956  dffv2  7003  fvco4i  7009  fvmptss  7027  fvmptex  7029  fvmptss2  7041  fvmptrabfv  7047  f0cli  7117  fvunsn  7198  fconst5  7225  csbriota  7402  riotassuni  7427  oprabidw  7461  csbov123  7474  csbov  7475  fvmptopab  7486  fvmptopabOLD  7487  brfvopab  7489  elimdelov  7528  ovif12  7532  ndmovcl  7617  ndmovord  7622  elovmpt3imp  7689  difsnexi  7779  ordsuc  7832  ordsucOLD  7833  ordsucelsuc  7841  1stval  8014  2ndval  8015  1st2val  8040  2nd2val  8041  el2mpocsbcl  8108  bropopvvv  8113  bropfvvvvlem  8114  bropfvvvv  8115  suppimacnv  8197  suppssdm  8200  ressuppss  8206  suppun  8207  extmptsuppeq  8211  funsssuppss  8213  fczsupp0  8216  suppss  8217  suppss2  8223  suppssfv  8225  suppco  8229  mpoxopynvov0  8241  mpoxopoveqd  8244  pwuninel  8298  smofvon2  8394  om0x  8555  mapssfset  8889  brdomg  8995  brdomgOLD  8996  snfi  9081  snfiOLD  9082  sdomirr  9152  domunsn  9165  2pwuninel  9170  unfi  9209  cnvfi  9214  snnen2oOLD  9261  suppeqfsuppbi  9416  fsuppun  9424  funsnfsupp  9429  fipwuni  9463  oicl  9566  oif  9567  wemapso2  9590  card2on  9591  en2lp  9643  ttrclselem1  9762  tctr  9777  r1tr  9813  rankdmr1  9838  r1pw  9882  r1pwALT  9883  rankuni  9900  scottex  9922  cardidm  9996  alephcard  10107  alephnbtwn  10108  cfub  10286  cardcf  10289  cflecard  10290  cfle  10291  cflim2  10300  cfidm  10312  isf32lem9  10398  itunisuc  10456  itunitc1  10457  itunitc  10458  ituniiun  10459  axcc2lem  10473  alephreg  10619  pwcfsdom  10620  cfpwsdom  10621  axunndlem1  10632  axpownd  10638  tskmcl  10878  addcompi  10931  addasspi  10932  mulcompi  10933  mulasspi  10934  distrpi  10935  addnidpi  10938  nlt1pi  10943  addcompq  10987  addcomnq  10988  mulcompq  10989  mulcomnq  10990  adderpq  10993  mulerpq  10994  addassnq  10995  mulassnq  10996  distrnq  10998  genpass  11046  addcompr  11058  mulcompr  11060  distrpr  11065  ltexprlem7  11079  addcomsr  11124  addasssr  11125  mulcomsr  11126  mulasssr  11127  distrsr  11128  uzssz  12896  uzwo  12950  nn01to3  12980  xnn0xaddcl  13273  elixx3g  13396  iooid  13411  elfz2  13550  injresinjlem  13822  injresinj  13823  fleqceilz  13890  modifeq2int  13970  modfzo0difsn  13980  addmodlteq  13983  ltweuz  13998  fzofi  14011  fsuppmapnn0fiubex  14029  hashrabrsn  14407  hashrabsn01  14408  hashrabsn1  14409  elprchashprn2  14431  hashss  14444  hashsn01  14451  hash1snb  14454  hashgt12el  14457  hashgt12el2  14458  hashgt23el  14459  hashfzp1  14466  hashfundm  14477  hash2pwpr  14511  hashge2el2dif  14515  hash3tpde  14528  ffz0iswrd  14575  ccatsymb  14616  swrd00  14678  swrd0  14692  swrdwrdsymb  14696  pfx00  14708  pfx0  14709  repswswrd  14818  0csh0  14827  cshwcl  14832  cshwidxmod  14837  repswcshw  14846  cshw1  14856  s3sndisj  15002  s3iunsndisj  15003  xptrrel  15015  trclfvcotrg  15051  relexpfld  15084  reusq0  15497  modfsummods  15825  dvdsaddre2b  16340  gcdaddmlem  16557  prm23ge5  16848  pcmptcl  16924  prmgaplem5  17088  prmgaplem6  17089  cshwshash  17138  strle1  17191  strfvss  17220  strfvi  17223  setsnid  17242  setsnidOLD  17243  ressbas  17279  ressbasOLD  17280  ressbasssg  17281  ressbasssOLD  17284  resseqnbas  17286  resslemOLD  17287  ress0  17288  ressress  17293  0rest  17475  firest  17478  topnval  17480  xpsaddlem  17619  xpsvsca  17623  homffval  17734  comfffval  17742  oppchomfval  17758  oppchomfvalOLD  17759  oppcbas  17763  oppcbasOLD  17764  fullfunc  17959  fthfunc  17960  natfval  18000  fucbas  18015  fuchom  18016  fuchomOLD  18017  arwval  18096  coafval  18117  xpcbas  18233  xpchomfval  18234  xpccofval  18237  oduval  18344  oduleval  18345  lubfun  18409  glbfun  18422  odujoin  18465  odumeet  18467  ipopos  18593  plusffval  18671  grpidval  18686  gsum0  18709  frmdplusg  18879  frmd0  18885  efmndbas  18896  efmndbasabf  18897  efmndplusg  18905  mgm2nsgrplem2  18944  mgm2nsgrplem3  18945  sgrp2rid2  18951  dfgrp2e  18993  grpinvfval  19008  grpinvfvalALT  19009  grpinvfvi  19012  grpsubfval  19013  grpsubfvalALT  19014  mulgfval  19099  mulgfvalALT  19100  mulgfvi  19103  cntrval  19349  oppgval  19377  oppgplusfval  19378  symgval  19402  snsymgefmndeq  19426  psgnfval  19532  odfval  19564  odfvalALT  19565  oppglsm  19674  efgval  19749  mgpval  20154  mgpplusg  20155  ringidval  20200  opprval  20351  opprmulfval  20352  dvdsrval  20377  invrfval  20405  dvrfval  20418  rrgval  20713  staffval  20858  scaffval  20894  rlmval  21215  rlmsca2  21223  2idlval  21278  nzerooringczr  21508  zrhval  21535  zlmlem  21544  zlmlemOLD  21545  zlmvsca  21553  chrval  21555  evpmss  21621  psgndiflemB  21635  ipffval  21683  thlbas  21731  thlbasOLD  21732  thlle  21733  thlleOLD  21734  thloc  21736  pjfval  21743  dsmmval2  21773  asclfval  21916  psrplusg  21973  psrmulr  21979  psrvscafval  21985  mplval  22026  mplcoe3  22073  evlval  22136  psr1val  22202  vr1val  22208  ply1val  22210  ply1basfvi  22257  ply1plusgfvi  22258  psr1sca2  22267  ply1sca2  22270  ply1ascl  22276  cply1mul  22315  gsummoncoe1  22327  evl1fval  22347  evl1fval1  22350  mamufacex  22415  mavmulsolcl  22572  marrepfval  22581  marepvfval  22586  submafval  22600  mdetfval  22607  mdetfval1  22611  mdetunilem7  22639  mdetunilem8  22640  madufval  22658  minmar1fval  22667  mp2pm2mplem4  22830  toponsspwpw  22943  tgdif0  23014  indislem  23022  resstopn  23209  iocpnfordt  23238  icomnfordt  23239  hmeofval  23781  ussval  24283  nmfval  24616  nghmfval  24758  pcofval  25056  tcphval  25265  ioombl  25613  ibladdlem  25869  itgaddlem1  25872  iblabs  25878  dvbsss  25951  perfdvf  25952  mdegfval  26115  deg1fval  26133  deg1fvi  26138  uc1pval  26193  mon1pval  26195  2irrexpq  26787  lgsqrmodndvds  27411  gausslemma2dlem1a  27423  2lgs  27465  2sqreultblem  27506  2sqreunnltblem  27509  newval  27908  leftval  27916  rightval  27917  lltropt  27925  oldssmade  27930  lrold  27949  ttglem  28899  ttglemOLD  28900  axcontlem12  29004  vtxval  29031  iedgval  29032  edgval  29080  usgr1v  29287  nbuhgr  29374  nbumgr  29378  uhgrnbgr0nb  29385  nbgr1vtx  29389  nbgrnself2  29391  nbusgrvtxm1  29410  sizusglecusg  29495  g0wlk0  29684  wlkreslem  29701  lfgrwlkprop  29719  wwlks  29864  wwlksn  29866  wspthsn  29877  iswwlksnon  29882  iswspthsnon  29885  0enwwlksnge1  29893  wwlksnfi  29935  clwwlk  30011  umgrclwwlkge2  30019  clwlkclwwlklem2a4  30025  clwwlkn  30054  clwwlknonmpo  30117  clwwlknon  30118  clwwlk0on0  30120  clwwlknon1le1  30129  1conngr  30222  eupth2lem3lem7  30262  frgr1v  30299  nfrgr2v  30300  1to2vfriswmgr  30307  2wspmdisj  30365  frgrreggt1  30421  frgrreg  30422  frgrregord013  30423  frgrogt3nreg  30425  friendship  30427  avril1  30491  vafval  30631  bafval  30632  smfval  30633  vsfval  30661  bcsiALT  31207  of0r  32694  fracval  33285  fracbas  33286  resvsca  33335  resvlem  33336  resvlemOLD  33337  cntnevol  34208  signsw0glem  34546  bnj1189  35001  fmlafvel  35369  gonan0  35376  satffun  35393  mvtval  35484  mexval  35486  mexval2  35487  mdvval  35488  mrsubfval  35492  mrsubrn  35497  msubfval  35508  elmsubrn  35512  msubrn  35513  mvhfval  35517  mpstval  35519  msrfval  35521  mstaval  35528  mppsval  35556  mthmval  35559  dfrdg3  35777  fvsingle  35901  unisnif  35906  funpartfv  35926  fullfunfv  35928  linedegen  36124  bj-ax6e  36650  axc11n11r  36665  bj-ax12v3ALT  36668  bj-sbsb  36819  bj-nfcsym  36881  bj-snex  37017  bj-restsnid  37069  bj-inftyexpitaudisj  37187  bj-inftyexpidisj  37192  finxpreclem4  37376  finxp00  37384  isinf2  37387  wl-nfs1t  37517  matunitlindflem1  37602  itg2addnclem  37657  ibladdnclem  37662  itgaddnclem1  37664  iblabsnc  37670  iblmulc2nc  37671  ftc1anclem8  37686  ismgmOLD  37836  tsbi1  38119  tsbi2  38120  ac6s6  38158  equid1  38880  ax12fromc15  38886  equid1ALT  38906  dvelimf-o  38910  ax12inda2ALT  38927  ax12inda2  38928  sn-axprlem3  42234  fsuppind  42576  mzpmfp  42734  itgocn  43152  mendbas  43168  mendplusgfval  43169  mendmulrfval  43171  mendsca  43173  mendvscafval  43174  arearect  43203  areaquad  43204  fpwfvss  43401  safesnsupfidom1o  43406  sn1dom  43515  or3or  44012  uneqsn  44014  addcomgi  44451  ax6e2ndeq  44556  2sb5ndVD  44907  2sb5ndALT  44929  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  hspdifhsp  46571  hspmbllem2  46582  hspmbl  46584  et-ltneverrefl  46826  tz6.12-afv  47122  ndmaovcl  47152  tz6.12-afv2  47189  otiunsndisjX  47228  fvmptrab  47241  nltle2tri  47262  fzopredsuc  47272  iccpartiltu  47346  iccpartigtl  47347  iccpartlt  47348  icceuelpartlem  47359  iccpartnel  47362  elsprel  47399  sprssspr  47405  sprsymrelfvlem  47414  prprelprb  47441  prprspr2  47442  fmtnoprmfac1  47489  fmtnoprmfac2  47491  prmdvdsfmtnof1lem2  47509  prminf2  47512  lighneallem4  47534  requad1  47546  requad2  47547  evenprm2  47638  even3prm2  47643  fpprbasnn  47653  stgoldbwt  47700  uspgrimprop  47810  upwlkbprop  47981  pgrpgt2nabl  48210  suppmptcfin  48220  linc1  48270  lindslinindsimp2lem5  48307  1aryenef  48494  2aryenef  48505  reorelicc  48559  rrxsphere  48597  fvconst0ci  48688  fvconstdomi  48689  setrec2lem1  48923  setrec2mpt  48927