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  1033  4cases  1041  pm4.42  1054  ifpid  1077  elimh  1083  3ecase  1476  norass  1537  ax6e  2388  ax12  2428  exdistrf  2452  equvini  2460  ax12vALT  2474  2ax6e  2476  sb1  2483  sb2  2484  sb4a  2485  dfsb1  2486  dfsb2  2498  sbcom3  2511  sbco2  2516  sbco3  2518  sb9  2524  eujustALT  2572  pm2.61ine  3025  ralcom2  3377  eueq2  3716  moeq3  3718  mo2icl  3720  sbc2or  3797  unineq  4288  csb0  4410  sbcel12  4411  sbcne12  4415  sbcel2  4418  csbidm  4433  csbun  4441  csbin  4442  csbdif  4524  ifsb  4539  ifid  4566  ifnot  4578  ifan  4579  ifor  4580  csbif  4583  elimhyp  4591  elimhyp2v  4592  elimhyp3v  4593  elimhyp4v  4594  elimdhyp  4596  keephyp2v  4598  keephyp3v  4599  rmosn  4719  rabsnif  4723  tppreqb  4805  ssunsn2  4827  n0snor2el  4833  preq12nebg  4863  opthprneg  4865  elpreqprlem  4866  dfopif  4870  csbuni  4936  disjord  5132  sbcbr  5198  unisn2  5312  intabs  5349  class2set  5355  dtruALT2  5370  snexALT  5383  dtruALT  5388  axprlem3  5425  axprlem3OLD  5428  snex  5436  exneq  5440  dtruOLD  5446  copsexgw  5495  copsexg  5496  snopeqop  5511  csbopab  5560  dfid3  5581  csbxp  5785  csbres  6000  csbima12  6097  soirri  6146  csbrn  6223  dmsnopss  6234  dmsnsnsn  6240  opswap  6249  unixpid  6304  predres  6360  nsuceq0  6467  ordsssuc2  6475  iotassuni  6533  iotaex  6534  iotassuniOLD  6540  iotaexOLD  6541  csbiota  6554  dffv3  6902  fvrn0  6936  ndmfv  6941  elfv2ex  6952  fveqres  6953  csbfv12  6954  csbfv  6956  dffv2  7004  fvco4i  7010  fvmptss  7028  fvmptex  7030  fvmptss2  7042  fvmptrabfv  7048  f0cli  7118  fvunsn  7199  fconst5  7226  csbriota  7403  riotassuni  7428  oprabidw  7462  csbov123  7475  csbov  7476  fvmptopab  7487  fvmptopabOLD  7488  brfvopab  7490  elimdelov  7529  ovif12  7533  ifmpt2v  7535  ndmovcl  7618  ndmovord  7623  elovmpt3imp  7690  difsnexi  7781  ordsuc  7833  ordsucOLD  7834  ordsucelsuc  7842  1stval  8016  2ndval  8017  1st2val  8042  2nd2val  8043  el2mpocsbcl  8110  bropopvvv  8115  bropfvvvvlem  8116  bropfvvvv  8117  suppimacnv  8199  suppssdm  8202  ressuppss  8208  suppun  8209  extmptsuppeq  8213  funsssuppss  8215  fczsupp0  8218  suppss  8219  suppss2  8225  suppssfv  8227  suppco  8231  mpoxopynvov0  8243  mpoxopoveqd  8246  pwuninel  8300  smofvon2  8396  om0x  8557  mapssfset  8891  brdomg  8997  brdomgOLD  8998  snfi  9083  snfiOLD  9084  sdomirr  9154  domunsn  9167  2pwuninel  9172  unfi  9211  cnvfi  9216  snnen2oOLD  9264  suppeqfsuppbi  9419  fsuppun  9427  funsnfsupp  9432  fipwuni  9466  oicl  9569  oif  9570  wemapso2  9593  card2on  9594  en2lp  9646  ttrclselem1  9765  tctr  9780  r1tr  9816  rankdmr1  9841  r1pw  9885  r1pwALT  9886  rankuni  9903  scottex  9925  cardidm  9999  alephcard  10110  alephnbtwn  10111  cfub  10289  cardcf  10292  cflecard  10293  cfle  10294  cflim2  10303  cfidm  10315  isf32lem9  10401  itunisuc  10459  itunitc1  10460  itunitc  10461  ituniiun  10462  axcc2lem  10476  alephreg  10622  pwcfsdom  10623  cfpwsdom  10624  axunndlem1  10635  axpownd  10641  tskmcl  10881  addcompi  10934  addasspi  10935  mulcompi  10936  mulasspi  10937  distrpi  10938  addnidpi  10941  nlt1pi  10946  addcompq  10990  addcomnq  10991  mulcompq  10992  mulcomnq  10993  adderpq  10996  mulerpq  10997  addassnq  10998  mulassnq  10999  distrnq  11001  genpass  11049  addcompr  11061  mulcompr  11063  distrpr  11068  ltexprlem7  11082  addcomsr  11127  addasssr  11128  mulcomsr  11129  mulasssr  11130  distrsr  11131  uzssz  12899  uzwo  12953  nn01to3  12983  xnn0xaddcl  13277  elixx3g  13400  iooid  13415  elfz2  13554  injresinjlem  13826  injresinj  13827  fleqceilz  13894  modifeq2int  13974  modfzo0difsn  13984  addmodlteq  13987  ltweuz  14002  fzofi  14015  fsuppmapnn0fiubex  14033  hashrabrsn  14411  hashrabsn01  14412  hashrabsn1  14413  elprchashprn2  14435  hashss  14448  hashsn01  14455  hash1snb  14458  hashgt12el  14461  hashgt12el2  14462  hashgt23el  14463  hashfzp1  14470  hashfundm  14481  hash2pwpr  14515  hashge2el2dif  14519  hash3tpde  14532  ffz0iswrd  14579  ccatsymb  14620  swrd00  14682  swrd0  14696  swrdwrdsymb  14700  pfx00  14712  pfx0  14713  repswswrd  14822  0csh0  14831  cshwcl  14836  cshwidxmod  14841  repswcshw  14850  cshw1  14860  s3sndisj  15006  s3iunsndisj  15007  xptrrel  15019  trclfvcotrg  15055  relexpfld  15088  reusq0  15501  modfsummods  15829  dvdsaddre2b  16344  gcdaddmlem  16561  prm23ge5  16853  pcmptcl  16929  prmgaplem5  17093  prmgaplem6  17094  cshwshash  17142  strle1  17195  strfvss  17224  strfvi  17227  setsnid  17245  setsnidOLD  17246  ressbas  17280  ressbasOLD  17281  ressbasssg  17282  ressbasssOLD  17285  resseqnbas  17287  resslemOLD  17288  ress0  17289  ressress  17293  0rest  17474  firest  17477  topnval  17479  xpsaddlem  17618  xpsvsca  17622  homffval  17733  comfffval  17741  oppchomfval  17757  oppcbas  17761  fullfunc  17953  fthfunc  17954  natfval  17994  fucbas  18008  fuchom  18009  arwval  18088  coafval  18109  xpcbas  18223  xpchomfval  18224  xpccofval  18227  oduval  18333  oduleval  18334  lubfun  18397  glbfun  18410  odujoin  18453  odumeet  18455  ipopos  18581  plusffval  18659  grpidval  18674  gsum0  18697  frmdplusg  18867  frmd0  18873  efmndbas  18884  efmndbasabf  18885  efmndplusg  18893  mgm2nsgrplem2  18932  mgm2nsgrplem3  18933  sgrp2rid2  18939  dfgrp2e  18981  grpinvfval  18996  grpinvfvalALT  18997  grpinvfvi  19000  grpsubfval  19001  grpsubfvalALT  19002  mulgfval  19087  mulgfvalALT  19088  mulgfvi  19091  cntrval  19337  oppgval  19365  oppgplusfval  19366  symgval  19388  snsymgefmndeq  19412  psgnfval  19518  odfval  19550  odfvalALT  19551  oppglsm  19660  efgval  19735  mgpval  20140  mgpplusg  20141  ringidval  20180  opprval  20335  opprmulfval  20336  dvdsrval  20361  invrfval  20389  dvrfval  20402  rrgval  20697  staffval  20842  scaffval  20878  rlmval  21198  rlmsca2  21206  2idlval  21261  nzerooringczr  21491  zrhval  21518  zlmlem  21527  zlmlemOLD  21528  zlmvsca  21536  chrval  21538  evpmss  21604  psgndiflemB  21618  ipffval  21666  thlbas  21714  thlbasOLD  21715  thlle  21716  thlleOLD  21717  thloc  21719  pjfval  21726  dsmmval2  21756  asclfval  21899  psrplusg  21956  psrmulr  21962  psrvscafval  21968  mplval  22009  mplcoe3  22056  evlval  22119  psr1val  22187  vr1val  22193  ply1val  22195  ply1basfvi  22242  ply1plusgfvi  22243  psr1sca2  22252  ply1sca2  22255  ply1ascl  22261  cply1mul  22300  gsummoncoe1  22312  evl1fval  22332  evl1fval1  22335  mamufacex  22400  mavmulsolcl  22557  marrepfval  22566  marepvfval  22571  submafval  22585  mdetfval  22592  mdetfval1  22596  mdetunilem7  22624  mdetunilem8  22625  madufval  22643  minmar1fval  22652  mp2pm2mplem4  22815  toponsspwpw  22928  tgdif0  22999  indislem  23007  resstopn  23194  iocpnfordt  23223  icomnfordt  23224  hmeofval  23766  ussval  24268  nmfval  24601  nghmfval  24743  pcofval  25043  tcphval  25252  ioombl  25600  ibladdlem  25855  itgaddlem1  25858  iblabs  25864  dvbsss  25937  perfdvf  25938  mdegfval  26101  deg1fval  26119  deg1fvi  26124  uc1pval  26179  mon1pval  26181  2irrexpq  26773  lgsqrmodndvds  27397  gausslemma2dlem1a  27409  2lgs  27451  2sqreultblem  27492  2sqreunnltblem  27495  newval  27894  leftval  27902  rightval  27903  lltropt  27911  oldssmade  27916  lrold  27935  ttglem  28885  ttglemOLD  28886  axcontlem12  28990  vtxval  29017  iedgval  29018  edgval  29066  usgr1v  29273  nbuhgr  29360  nbumgr  29364  uhgrnbgr0nb  29371  nbgr1vtx  29375  nbgrnself2  29377  nbusgrvtxm1  29396  sizusglecusg  29481  g0wlk0  29670  wlkreslem  29687  lfgrwlkprop  29705  wwlks  29855  wwlksn  29857  wspthsn  29868  iswwlksnon  29873  iswspthsnon  29876  0enwwlksnge1  29884  wwlksnfi  29926  clwwlk  30002  umgrclwwlkge2  30010  clwlkclwwlklem2a4  30016  clwwlkn  30045  clwwlknonmpo  30108  clwwlknon  30109  clwwlk0on0  30111  clwwlknon1le1  30120  1conngr  30213  eupth2lem3lem7  30253  frgr1v  30290  nfrgr2v  30291  1to2vfriswmgr  30298  2wspmdisj  30356  frgrreggt1  30412  frgrreg  30413  frgrregord013  30414  frgrogt3nreg  30416  friendship  30418  avril1  30482  vafval  30622  bafval  30623  smfval  30624  vsfval  30652  bcsiALT  31198  of0r  32688  fracval  33306  fracbas  33307  resvsca  33356  resvlem  33357  resvlemOLD  33358  cntnevol  34229  signsw0glem  34568  bnj1189  35023  fmlafvel  35390  gonan0  35397  satffun  35414  mvtval  35505  mexval  35507  mexval2  35508  mdvval  35509  mrsubfval  35513  mrsubrn  35518  msubfval  35529  elmsubrn  35533  msubrn  35534  mvhfval  35538  mpstval  35540  msrfval  35542  mstaval  35549  mppsval  35577  mthmval  35580  dfrdg3  35797  fvsingle  35921  unisnif  35926  funpartfv  35946  fullfunfv  35948  linedegen  36144  bj-ax6e  36669  axc11n11r  36684  bj-ax12v3ALT  36687  bj-sbsb  36838  bj-nfcsym  36900  bj-snex  37036  bj-restsnid  37088  bj-inftyexpitaudisj  37206  bj-inftyexpidisj  37211  finxpreclem4  37395  finxp00  37403  isinf2  37406  wl-nfs1t  37538  matunitlindflem1  37623  itg2addnclem  37678  ibladdnclem  37683  itgaddnclem1  37685  iblabsnc  37691  iblmulc2nc  37692  ftc1anclem8  37707  ismgmOLD  37857  tsbi1  38140  tsbi2  38141  ac6s6  38179  equid1  38900  ax12fromc15  38906  equid1ALT  38926  dvelimf-o  38930  ax12inda2ALT  38947  ax12inda2  38948  sn-axprlem3  42256  fsuppind  42600  mzpmfp  42758  itgocn  43176  mendbas  43192  mendplusgfval  43193  mendmulrfval  43195  mendsca  43197  mendvscafval  43198  arearect  43227  areaquad  43228  fpwfvss  43425  safesnsupfidom1o  43430  sn1dom  43539  or3or  44036  uneqsn  44038  addcomgi  44475  ax6e2ndeq  44579  2sb5ndVD  44930  2sb5ndALT  44952  sqwvfoura  46243  sqwvfourb  46244  fourierswlem  46245  fouriersw  46246  hspdifhsp  46631  hspmbllem2  46642  hspmbl  46644  et-ltneverrefl  46886  tz6.12-afv  47185  ndmaovcl  47215  tz6.12-afv2  47252  otiunsndisjX  47291  fvmptrab  47304  nltle2tri  47325  fzopredsuc  47335  iccpartiltu  47409  iccpartigtl  47410  iccpartlt  47411  icceuelpartlem  47422  iccpartnel  47425  elsprel  47462  sprssspr  47468  sprsymrelfvlem  47477  prprelprb  47504  prprspr2  47505  fmtnoprmfac1  47552  fmtnoprmfac2  47554  prmdvdsfmtnof1lem2  47572  prminf2  47575  lighneallem4  47597  requad1  47609  requad2  47610  evenprm2  47701  even3prm2  47706  fpprbasnn  47716  stgoldbwt  47763  uspgrimprop  47873  upwlkbprop  48054  pgrpgt2nabl  48282  suppmptcfin  48292  linc1  48342  lindslinindsimp2lem5  48379  1aryenef  48566  2aryenef  48577  reorelicc  48631  rrxsphere  48669  fvconst0ci  48790  fvconstdomi  48791  upfval  48933  setrec2lem1  49212  setrec2mpt  49216