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  1538  ax6e  2383  ax12  2423  exdistrf  2447  equvini  2455  ax12vALT  2469  2ax6e  2471  sb1  2478  sb2  2479  sb4a  2480  dfsb1  2481  dfsb2  2493  sbcom3  2506  sbco2  2511  sbco3  2513  sb9  2519  eujustALT  2567  pm2.61ine  3011  ralcom2  3343  eueq2  3664  moeq3  3666  mo2icl  3668  sbc2or  3745  unineq  4235  csb0  4357  sbcel12  4358  sbcne12  4362  sbcel2  4365  csbidm  4380  csbun  4388  csbin  4389  csbdif  4471  ifsb  4486  ifid  4513  ifnot  4525  ifan  4526  ifor  4527  csbif  4530  elimhyp  4538  elimhyp2v  4539  elimhyp3v  4540  elimhyp4v  4541  elimdhyp  4543  keephyp2v  4545  keephyp3v  4546  rmosn  4669  rabsnif  4673  tppreqb  4754  ssunsn2  4776  n0snor2el  4782  preq12nebg  4812  opthprneg  4814  elpreqprlem  4815  dfopif  4819  csbuni  4886  disjord  5078  sbcbr  5144  unisn2  5248  intabs  5285  class2set  5291  dtruALT2  5306  snexALT  5319  dtruALT  5324  axprlem3  5361  axprlem3OLD  5364  snex  5372  exneq  5376  copsexgw  5428  copsexg  5429  snopeqop  5444  csbopab  5493  dfid3  5512  csbxp  5715  csbres  5930  csbima12  6027  soirri  6072  csbrn  6150  dmsnopss  6161  dmsnsnsn  6167  opswap  6176  unixpid  6231  predres  6286  nsuceq0  6391  ordsssuc2  6399  iotassuni  6456  iotaex  6457  csbiota  6474  dffv3  6818  fvrn0  6850  ndmfv  6854  elfv2ex  6865  fveqres  6866  csbfv12  6867  csbfv  6869  dffv2  6917  fvco4i  6923  fvmptss  6941  fvmptex  6943  fvmptss2  6955  fvmptrabfv  6961  f0cli  7031  fvunsn  7113  fconst5  7140  csbriota  7318  riotassuni  7343  oprabidw  7377  csbov123  7390  csbov  7391  fvmptopab  7401  brfvopab  7403  elimdelov  7442  ovif12  7446  ifmpt2v  7448  ndmovcl  7531  ndmovord  7536  elovmpt3imp  7603  difsnexi  7694  ordsuc  7744  ordsucelsuc  7752  1stval  7923  2ndval  7924  1st2val  7949  2nd2val  7950  el2mpocsbcl  8015  bropopvvv  8020  bropfvvvvlem  8021  bropfvvvv  8022  suppimacnv  8104  suppssdm  8107  ressuppss  8113  suppun  8114  extmptsuppeq  8118  funsssuppss  8120  fczsupp0  8123  suppss  8124  suppss2  8130  suppssfv  8132  suppco  8136  mpoxopynvov0  8148  mpoxopoveqd  8151  pwuninel  8205  smofvon2  8276  om0x  8434  mapssfset  8775  brdomg  8881  snfi  8965  sdomirr  9027  domunsn  9040  2pwuninel  9045  unfi  9080  cnvfi  9085  suppeqfsuppbi  9263  fsuppun  9271  funsnfsupp  9276  fipwuni  9310  oicl  9415  oif  9416  wemapso2  9439  card2on  9440  en2lp  9496  ttrclselem1  9615  tctr  9628  r1tr  9669  rankdmr1  9694  r1pw  9738  r1pwALT  9739  rankuni  9756  scottex  9778  cardidm  9852  alephcard  9961  alephnbtwn  9962  cfub  10140  cardcf  10143  cflecard  10144  cfle  10145  cflim2  10154  cfidm  10166  isf32lem9  10252  itunisuc  10310  itunitc1  10311  itunitc  10312  ituniiun  10313  axcc2lem  10327  alephreg  10473  pwcfsdom  10474  cfpwsdom  10475  axunndlem1  10486  axpownd  10492  tskmcl  10732  addcompi  10785  addasspi  10786  mulcompi  10787  mulasspi  10788  distrpi  10789  addnidpi  10792  nlt1pi  10797  addcompq  10841  addcomnq  10842  mulcompq  10843  mulcomnq  10844  adderpq  10847  mulerpq  10848  addassnq  10849  mulassnq  10850  distrnq  10852  genpass  10900  addcompr  10912  mulcompr  10914  distrpr  10919  ltexprlem7  10933  addcomsr  10978  addasssr  10979  mulcomsr  10980  mulasssr  10981  distrsr  10982  uzssz  12753  uzwo  12809  nn01to3  12839  xnn0xaddcl  13134  elixx3g  13258  iooid  13273  elfz2  13414  injresinjlem  13690  injresinj  13691  fleqceilz  13758  modifeq2int  13840  modfzo0difsn  13850  addmodlteq  13853  ltweuz  13868  fzofi  13881  fsuppmapnn0fiubex  13899  hashrabrsn  14279  hashrabsn01  14280  hashrabsn1  14281  elprchashprn2  14303  hashss  14316  hashsn01  14323  hash1snb  14326  hashgt12el  14329  hashgt12el2  14330  hashgt23el  14331  hashfzp1  14338  hashfundm  14349  hash2pwpr  14383  hashge2el2dif  14387  hash3tpde  14400  ffz0iswrd  14448  ccatsymb  14490  swrd00  14552  swrd0  14566  swrdwrdsymb  14570  pfx00  14582  pfx0  14583  repswswrd  14691  0csh0  14700  cshwcl  14705  cshwidxmod  14710  repswcshw  14719  cshw1  14729  s3sndisj  14874  s3iunsndisj  14875  xptrrel  14887  trclfvcotrg  14923  relexpfld  14956  reusq0  15372  modfsummods  15700  dvdsaddre2b  16218  gcdaddmlem  16435  prm23ge5  16727  pcmptcl  16803  prmgaplem5  16967  prmgaplem6  16968  cshwshash  17016  strle1  17069  strfvss  17098  strfvi  17101  setsnid  17119  ressbas  17147  ressbasssg  17148  ressbasssOLD  17151  resseqnbas  17153  ress0  17154  ressress  17158  0rest  17333  firest  17336  topnval  17338  xpsaddlem  17477  xpsvsca  17481  homffval  17596  comfffval  17604  oppchomfval  17620  oppcbas  17624  fullfunc  17815  fthfunc  17816  natfval  17856  fucbas  17870  fuchom  17871  arwval  17950  coafval  17971  xpcbas  18084  xpchomfval  18085  xpccofval  18088  oduval  18194  oduleval  18195  lubfun  18256  glbfun  18269  odujoin  18312  odumeet  18314  ipopos  18442  plusffval  18554  grpidval  18569  gsum0  18592  frmdplusg  18762  frmd0  18768  efmndbas  18779  efmndbasabf  18780  efmndplusg  18788  mgm2nsgrplem2  18827  mgm2nsgrplem3  18828  sgrp2rid2  18834  dfgrp2e  18876  grpinvfval  18891  grpinvfvalALT  18892  grpinvfvi  18895  grpsubfval  18896  grpsubfvalALT  18897  mulgfval  18982  mulgfvalALT  18983  mulgfvi  18986  cntrval  19231  oppgval  19259  oppgplusfval  19260  symgval  19283  snsymgefmndeq  19307  psgnfval  19412  odfval  19444  odfvalALT  19445  oppglsm  19554  efgval  19629  mgpval  20061  mgpplusg  20062  ringidval  20101  opprval  20256  opprmulfval  20257  dvdsrval  20279  invrfval  20307  dvrfval  20320  rrgval  20612  staffval  20756  scaffval  20813  rlmval  21125  rlmsca2  21133  2idlval  21188  nzerooringczr  21417  zrhval  21444  zlmlem  21453  zlmvsca  21458  chrval  21460  evpmss  21523  psgndiflemB  21537  ipffval  21585  thlbas  21633  thlle  21634  thloc  21636  pjfval  21643  dsmmval2  21673  asclfval  21816  psrplusg  21873  psrmulr  21879  psrvscafval  21885  mplval  21926  mplcoe3  21973  evlval  22030  psr1val  22098  vr1val  22104  ply1val  22106  ply1basfvi  22153  ply1plusgfvi  22154  psr1sca2  22163  ply1sca2  22166  ply1ascl  22172  cply1mul  22211  gsummoncoe1  22223  evl1fval  22243  evl1fval1  22246  mamufacex  22311  mavmulsolcl  22466  marrepfval  22475  marepvfval  22480  submafval  22494  mdetfval  22501  mdetfval1  22505  mdetunilem7  22533  mdetunilem8  22534  madufval  22552  minmar1fval  22561  mp2pm2mplem4  22724  toponsspwpw  22837  tgdif0  22907  indislem  22915  resstopn  23101  iocpnfordt  23130  icomnfordt  23131  hmeofval  23673  ussval  24174  nmfval  24503  nghmfval  24637  pcofval  24937  tcphval  25145  ioombl  25493  ibladdlem  25748  itgaddlem1  25751  iblabs  25757  dvbsss  25830  perfdvf  25831  mdegfval  25994  deg1fval  26012  deg1fvi  26017  uc1pval  26072  mon1pval  26074  2irrexpq  26667  lgsqrmodndvds  27291  gausslemma2dlem1a  27303  2lgs  27345  2sqreultblem  27386  2sqreunnltblem  27389  newval  27796  leftval  27804  rightval  27805  lltropt  27817  oldssmade  27822  oldss  27823  lrold  27842  ttglem  28854  axcontlem12  28953  vtxval  28978  iedgval  28979  edgval  29027  usgr1v  29234  nbuhgr  29321  nbumgr  29325  uhgrnbgr0nb  29332  nbgr1vtx  29336  nbgrnself2  29338  nbusgrvtxm1  29357  sizusglecusg  29442  g0wlk0  29629  wlkreslem  29646  lfgrwlkprop  29664  wwlks  29813  wwlksn  29815  wspthsn  29826  iswwlksnon  29831  iswspthsnon  29834  0enwwlksnge1  29842  wwlksnfi  29884  clwwlk  29963  umgrclwwlkge2  29971  clwlkclwwlklem2a4  29977  clwwlkn  30006  clwwlknonmpo  30069  clwwlknon  30070  clwwlk0on0  30072  clwwlknon1le1  30081  1conngr  30174  eupth2lem3lem7  30214  frgr1v  30251  nfrgr2v  30252  1to2vfriswmgr  30259  2wspmdisj  30317  frgrreggt1  30373  frgrreg  30374  frgrregord013  30375  frgrogt3nreg  30377  friendship  30379  avril1  30443  vafval  30583  bafval  30584  smfval  30585  vsfval  30613  bcsiALT  31159  of0r  32660  fracval  33270  fracbas  33271  resvsca  33297  resvlem  33298  cntnevol  34241  signsw0glem  34566  bnj1189  35021  r1wf  35107  fmlafvel  35429  gonan0  35436  satffun  35453  mvtval  35544  mexval  35546  mexval2  35547  mdvval  35548  mrsubfval  35552  mrsubrn  35557  msubfval  35568  elmsubrn  35572  msubrn  35573  mvhfval  35577  mpstval  35579  msrfval  35581  mstaval  35588  mppsval  35616  mthmval  35619  antnestlaw2  35736  dfrdg3  35838  fvsingle  35962  unisnif  35967  funpartfv  35987  fullfunfv  35989  linedegen  36185  bj-ax6e  36710  axc11n11r  36725  bj-ax12v3ALT  36728  bj-sbsb  36879  bj-nfcsym  36941  bj-snex  37077  bj-restsnid  37129  bj-inftyexpitaudisj  37247  bj-inftyexpidisj  37252  finxpreclem4  37436  finxp00  37444  isinf2  37447  wl-nfs1t  37579  matunitlindflem1  37664  itg2addnclem  37719  ibladdnclem  37724  itgaddnclem1  37726  iblabsnc  37732  iblmulc2nc  37733  ftc1anclem8  37748  ismgmOLD  37898  tsbi1  38181  tsbi2  38182  ac6s6  38220  equid1  38946  ax12fromc15  38952  equid1ALT  38972  dvelimf-o  38976  ax12inda2ALT  38993  ax12inda2  38994  sn-axprlem3  42258  fsuppind  42631  mzpmfp  42788  itgocn  43205  mendbas  43221  mendplusgfval  43222  mendmulrfval  43224  mendsca  43226  mendvscafval  43227  arearect  43256  areaquad  43257  fpwfvss  43453  safesnsupfidom1o  43458  sn1dom  43567  or3or  44064  uneqsn  44066  addcomgi  44496  ax6e2ndeq  44600  2sb5ndVD  44950  2sb5ndALT  44972  sqwvfoura  46274  sqwvfourb  46275  fourierswlem  46276  fouriersw  46277  hspdifhsp  46662  hspmbllem2  46673  hspmbl  46675  et-ltneverrefl  46917  tz6.12-afv  47212  ndmaovcl  47242  tz6.12-afv2  47279  otiunsndisjX  47318  fvmptrab  47331  nltle2tri  47352  fzopredsuc  47362  iccpartiltu  47461  iccpartigtl  47462  iccpartlt  47463  icceuelpartlem  47474  iccpartnel  47477  elsprel  47514  sprssspr  47520  sprsymrelfvlem  47529  prprelprb  47556  prprspr2  47557  fmtnoprmfac1  47604  fmtnoprmfac2  47606  prmdvdsfmtnof1lem2  47624  prminf2  47627  lighneallem4  47649  requad1  47661  requad2  47662  evenprm2  47753  even3prm2  47758  fpprbasnn  47768  stgoldbwt  47815  pgnbgreunbgrlem2lem1  48153  pgnbgreunbgrlem2lem2  48154  pgnbgreunbgrlem2lem3  48155  upwlkbprop  48177  pgrpgt2nabl  48405  suppmptcfin  48415  linc1  48465  lindslinindsimp2lem5  48502  1aryenef  48685  2aryenef  48696  reorelicc  48750  rrxsphere  48788  fvconst0ci  48930  fvconstdomi  48931  upfval  49216  reldmprcof1  49421  reldmprcof2  49422  lmdfval  49689  cmdfval  49690  setrec2lem1  49733  setrec2mpt  49737