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  1477  norass  1539  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  2573  pm2.61ine  3016  ralcom2  3349  eueq2  3670  moeq3  3672  mo2icl  3674  sbc2or  3751  unineq  4242  csb0  4364  sbcel12  4365  sbcne12  4369  sbcel2  4372  csbidm  4387  csbun  4395  csbin  4396  csbdif  4480  ifsb  4495  ifid  4522  ifnot  4534  ifan  4535  ifor  4536  csbif  4539  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elimdhyp  4552  keephyp2v  4554  keephyp3v  4555  rmosn  4678  rabsnif  4682  tppreqb  4763  ssunsn2  4785  n0snor2el  4791  preq12nebg  4821  opthprneg  4823  elpreqprlem  4824  dfopif  4828  csbuni  4895  disjord  5089  sbcbr  5155  unisn2  5259  intabs  5296  class2set  5302  dtruALT2  5317  snexALT  5330  dtruALT  5335  axprlem3  5372  axprlem3OLD  5375  axprglem  5382  axprg  5383  snexOLD  5388  exneq  5392  copsexgw  5446  copsexg  5447  snopeqop  5462  csbopab  5511  dfid3  5530  csbxp  5733  csbres  5949  csbima12  6046  soirri  6091  csbrn  6169  dmsnopss  6180  dmsnsnsn  6186  opswap  6195  unixpid  6250  predres  6305  nsuceq0  6410  ordsssuc2  6418  iotassuni  6475  iotaex  6476  csbiota  6493  dffv3  6838  fvrn0  6870  ndmfv  6874  elfv2ex  6885  fveqres  6886  csbfv12  6887  csbfv  6889  dffv2  6937  fvco4i  6943  fvmptss  6962  fvmptex  6964  fvmptss2  6976  fvmptrabfv  6982  f0cli  7052  fvunsn  7135  fconst5  7162  csbriota  7340  riotassuni  7365  oprabidw  7399  csbov123  7412  csbov  7413  fvmptopab  7423  brfvopab  7425  elimdelov  7464  ovif12  7468  ifmpt2v  7470  ndmovcl  7553  ndmovord  7558  elovmpt3imp  7625  difsnexi  7716  ordsuc  7766  ordsucelsuc  7774  1stval  7945  2ndval  7946  1st2val  7971  2nd2val  7972  el2mpocsbcl  8037  bropopvvv  8042  bropfvvvvlem  8043  bropfvvvv  8044  suppimacnv  8126  suppssdm  8129  ressuppss  8135  suppun  8136  extmptsuppeq  8140  funsssuppss  8142  fczsupp0  8145  suppss  8146  suppss2  8152  suppssfv  8154  suppco  8158  mpoxopynvov0  8170  mpoxopoveqd  8173  pwuninel  8227  smofvon2  8298  om0x  8456  mapssfset  8800  brdomg  8907  snfi  8992  sdomirr  9054  domunsn  9067  2pwuninel  9072  unfi  9107  cnvfi  9112  suppeqfsuppbi  9294  fsuppun  9302  funsnfsupp  9307  fipwuni  9341  oicl  9446  oif  9447  wemapso2  9470  card2on  9471  en2lp  9527  ttrclselem1  9646  tctr  9659  r1tr  9700  rankdmr1  9725  r1pw  9769  r1pwALT  9770  rankuni  9787  scottex  9809  cardidm  9883  alephcard  9992  alephnbtwn  9993  cfub  10171  cardcf  10174  cflecard  10175  cfle  10176  cflim2  10185  cfidm  10197  isf32lem9  10283  itunisuc  10341  itunitc1  10342  itunitc  10343  ituniiun  10344  axcc2lem  10358  alephreg  10505  pwcfsdom  10506  cfpwsdom  10507  axunndlem1  10518  axpownd  10524  tskmcl  10764  addcompi  10817  addasspi  10818  mulcompi  10819  mulasspi  10820  distrpi  10821  addnidpi  10824  nlt1pi  10829  addcompq  10873  addcomnq  10874  mulcompq  10875  mulcomnq  10876  adderpq  10879  mulerpq  10880  addassnq  10881  mulassnq  10882  distrnq  10884  genpass  10932  addcompr  10944  mulcompr  10946  distrpr  10951  ltexprlem7  10965  addcomsr  11010  addasssr  11011  mulcomsr  11012  mulasssr  11013  distrsr  11014  uzssz  12784  uzwo  12836  nn01to3  12866  xnn0xaddcl  13162  elixx3g  13286  iooid  13301  elfz2  13442  injresinjlem  13718  injresinj  13719  fleqceilz  13786  modifeq2int  13868  modfzo0difsn  13878  addmodlteq  13881  ltweuz  13896  fzofi  13909  fsuppmapnn0fiubex  13927  hashrabrsn  14307  hashrabsn01  14308  hashrabsn1  14309  elprchashprn2  14331  hashss  14344  hashsn01  14351  hash1snb  14354  hashgt12el  14357  hashgt12el2  14358  hashgt23el  14359  hashfzp1  14366  hashfundm  14377  hash2pwpr  14411  hashge2el2dif  14415  hash3tpde  14428  ffz0iswrd  14476  ccatsymb  14518  swrd00  14580  swrd0  14594  swrdwrdsymb  14598  pfx00  14610  pfx0  14611  repswswrd  14719  0csh0  14728  cshwcl  14733  cshwidxmod  14738  repswcshw  14747  cshw1  14757  s3sndisj  14902  s3iunsndisj  14903  xptrrel  14915  trclfvcotrg  14951  relexpfld  14984  reusq0  15400  modfsummods  15728  dvdsaddre2b  16246  gcdaddmlem  16463  prm23ge5  16755  pcmptcl  16831  prmgaplem5  16995  prmgaplem6  16996  cshwshash  17044  strle1  17097  strfvss  17126  strfvi  17129  setsnid  17147  ressbas  17175  ressbasssg  17176  ressbasssOLD  17179  resseqnbas  17181  ress0  17182  ressress  17186  0rest  17361  firest  17364  topnval  17366  xpsaddlem  17506  xpsvsca  17510  homffval  17625  comfffval  17633  oppchomfval  17649  oppcbas  17653  fullfunc  17844  fthfunc  17845  natfval  17885  fucbas  17899  fuchom  17900  arwval  17979  coafval  18000  xpcbas  18113  xpchomfval  18114  xpccofval  18117  oduval  18223  oduleval  18224  lubfun  18285  glbfun  18298  odujoin  18341  odumeet  18343  ipopos  18471  plusffval  18583  grpidval  18598  gsum0  18621  frmdplusg  18791  frmd0  18797  efmndbas  18808  efmndbasabf  18809  efmndplusg  18817  mgm2nsgrplem2  18856  mgm2nsgrplem3  18857  sgrp2rid2  18863  dfgrp2e  18905  grpinvfval  18920  grpinvfvalALT  18921  grpinvfvi  18924  grpsubfval  18925  grpsubfvalALT  18926  mulgfval  19011  mulgfvalALT  19012  mulgfvi  19015  cntrval  19260  oppgval  19288  oppgplusfval  19289  symgval  19312  snsymgefmndeq  19336  psgnfval  19441  odfval  19473  odfvalALT  19474  oppglsm  19583  efgval  19658  mgpval  20090  mgpplusg  20091  ringidval  20130  opprval  20286  opprmulfval  20287  dvdsrval  20309  invrfval  20337  dvrfval  20350  rrgval  20642  staffval  20786  scaffval  20843  rlmval  21155  rlmsca2  21163  2idlval  21218  nzerooringczr  21447  zrhval  21474  zlmlem  21483  zlmvsca  21488  chrval  21490  evpmss  21553  psgndiflemB  21567  ipffval  21615  thlbas  21663  thlle  21664  thloc  21666  pjfval  21673  dsmmval2  21703  asclfval  21846  psrplusg  21904  psrmulr  21910  psrvscafval  21916  mplval  21956  mplcoe3  22005  evlval  22067  psr1val  22138  vr1val  22144  ply1val  22146  ply1basfvi  22193  ply1plusgfvi  22194  psr1sca2  22203  ply1sca2  22206  ply1ascl  22212  cply1mul  22252  gsummoncoe1  22264  evl1fval  22284  evl1fval1  22287  mamufacex  22352  mavmulsolcl  22507  marrepfval  22516  marepvfval  22521  submafval  22535  mdetfval  22542  mdetfval1  22546  mdetunilem7  22574  mdetunilem8  22575  madufval  22593  minmar1fval  22602  mp2pm2mplem4  22765  toponsspwpw  22878  tgdif0  22948  indislem  22956  resstopn  23142  iocpnfordt  23171  icomnfordt  23172  hmeofval  23714  ussval  24215  nmfval  24544  nghmfval  24678  pcofval  24978  tcphval  25186  ioombl  25534  ibladdlem  25789  itgaddlem1  25792  iblabs  25798  dvbsss  25871  perfdvf  25872  mdegfval  26035  deg1fval  26053  deg1fvi  26058  uc1pval  26113  mon1pval  26115  2irrexpq  26708  lgsqrmodndvds  27332  gausslemma2dlem1a  27344  2lgs  27386  2sqreultblem  27427  2sqreunnltblem  27430  newval  27843  leftval  27857  rightval  27858  lltr  27870  oldssmade  27875  oldss  27878  lrold  27905  ttglem  28960  axcontlem12  29060  vtxval  29085  iedgval  29086  edgval  29134  usgr1v  29341  nbuhgr  29428  nbumgr  29432  uhgrnbgr0nb  29439  nbgr1vtx  29443  nbgrnself2  29445  nbusgrvtxm1  29464  sizusglecusg  29549  g0wlk0  29736  wlkreslem  29753  lfgrwlkprop  29771  wwlks  29920  wwlksn  29922  wspthsn  29933  iswwlksnon  29938  iswspthsnon  29941  0enwwlksnge1  29949  wwlksnfi  29991  clwwlk  30070  umgrclwwlkge2  30078  clwlkclwwlklem2a4  30084  clwwlkn  30113  clwwlknonmpo  30176  clwwlknon  30177  clwwlk0on0  30179  clwwlknon1le1  30188  1conngr  30281  eupth2lem3lem7  30321  frgr1v  30358  nfrgr2v  30359  1to2vfriswmgr  30366  2wspmdisj  30424  frgrreggt1  30480  frgrreg  30481  frgrregord013  30482  frgrogt3nreg  30484  friendship  30486  avril1  30550  vafval  30691  bafval  30692  smfval  30693  vsfval  30721  bcsiALT  31267  of0r  32769  fracval  33398  fracbas  33399  resvsca  33425  resvlem  33426  cntnevol  34406  signsw0glem  34731  bnj1189  35185  r1wf  35273  noinfepregs  35311  fmlafvel  35601  gonan0  35608  satffun  35625  mvtval  35716  mexval  35718  mexval2  35719  mdvval  35720  mrsubfval  35724  mrsubrn  35729  msubfval  35740  elmsubrn  35744  msubrn  35745  mvhfval  35749  mpstval  35751  msrfval  35753  mstaval  35760  mppsval  35788  mthmval  35791  antnestlaw2  35908  dfrdg3  36010  fvsingle  36134  unisnif  36139  funpartfv  36161  fullfunfv  36163  linedegen  36359  mh-setindnd  36689  bj-ax6e  36913  axc11n11r  36928  bj-ax12v3ALT  36931  bj-sbsb  37085  bj-nfcsym  37147  bj-snex  37283  bj-restsnid  37340  bj-inftyexpitaudisj  37460  bj-inftyexpidisj  37465  finxpreclem4  37649  finxp00  37657  isinf2  37660  wl-nfs1t  37792  matunitlindflem1  37867  itg2addnclem  37922  ibladdnclem  37927  itgaddnclem1  37929  iblabsnc  37935  iblmulc2nc  37936  ftc1anclem8  37951  ismgmOLD  38101  tsbi1  38384  tsbi2  38385  ac6s6  38423  equid1  39275  ax12fromc15  39281  equid1ALT  39301  dvelimf-o  39305  ax12inda2ALT  39322  ax12inda2  39323  sn-axprlem3  42590  fsuppind  42948  mzpmfp  43104  itgocn  43521  mendbas  43537  mendplusgfval  43538  mendmulrfval  43540  mendsca  43542  mendvscafval  43543  arearect  43572  areaquad  43573  fpwfvss  43768  safesnsupfidom1o  43773  sn1dom  43882  or3or  44379  uneqsn  44381  addcomgi  44811  ax6e2ndeq  44915  2sb5ndVD  45265  2sb5ndALT  45287  sqwvfoura  46586  sqwvfourb  46587  fourierswlem  46588  fouriersw  46589  hspdifhsp  46974  hspmbllem2  46985  hspmbl  46987  et-ltneverrefl  47229  tz6.12-afv  47533  ndmaovcl  47563  tz6.12-afv2  47600  otiunsndisjX  47639  fvmptrab  47652  nltle2tri  47673  fzopredsuc  47683  iccpartiltu  47782  iccpartigtl  47783  iccpartlt  47784  icceuelpartlem  47795  iccpartnel  47798  elsprel  47835  sprssspr  47841  sprsymrelfvlem  47850  prprelprb  47877  prprspr2  47878  fmtnoprmfac1  47925  fmtnoprmfac2  47927  prmdvdsfmtnof1lem2  47945  prminf2  47948  lighneallem4  47970  requad1  47982  requad2  47983  evenprm2  48074  even3prm2  48079  fpprbasnn  48089  stgoldbwt  48136  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  upwlkbprop  48498  pgrpgt2nabl  48726  suppmptcfin  48736  linc1  48785  lindslinindsimp2lem5  48822  1aryenef  49005  2aryenef  49016  reorelicc  49070  rrxsphere  49108  fvconst0ci  49250  fvconstdomi  49251  upfval  49535  reldmprcof1  49740  reldmprcof2  49741  lmdfval  50008  cmdfval  50009  setrec2lem1  50052  setrec2mpt  50056