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  1537  ax6e  2381  ax12  2421  exdistrf  2445  equvini  2453  ax12vALT  2467  2ax6e  2469  sb1  2476  sb2  2477  sb4a  2478  dfsb1  2479  dfsb2  2491  sbcom3  2504  sbco2  2509  sbco3  2511  sb9  2517  eujustALT  2565  pm2.61ine  3008  ralcom2  3340  eueq2  3670  moeq3  3672  mo2icl  3674  sbc2or  3751  unineq  4239  csb0  4361  sbcel12  4362  sbcne12  4366  sbcel2  4369  csbidm  4384  csbun  4392  csbin  4393  csbdif  4475  ifsb  4490  ifid  4517  ifnot  4529  ifan  4530  ifor  4531  csbif  4534  elimhyp  4542  elimhyp2v  4543  elimhyp3v  4544  elimhyp4v  4545  elimdhyp  4547  keephyp2v  4549  keephyp3v  4550  rmosn  4671  rabsnif  4675  tppreqb  4756  ssunsn2  4778  n0snor2el  4784  preq12nebg  4814  opthprneg  4816  elpreqprlem  4817  dfopif  4821  csbuni  4887  disjord  5081  sbcbr  5147  unisn2  5251  intabs  5288  class2set  5294  dtruALT2  5309  snexALT  5322  dtruALT  5327  axprlem3  5364  axprlem3OLD  5367  snex  5375  exneq  5379  copsexgw  5433  copsexg  5434  snopeqop  5449  csbopab  5498  dfid3  5517  csbxp  5719  csbres  5933  csbima12  6030  soirri  6075  csbrn  6152  dmsnopss  6163  dmsnsnsn  6169  opswap  6178  unixpid  6232  predres  6287  nsuceq0  6392  ordsssuc2  6400  iotassuni  6457  iotaex  6458  csbiota  6475  dffv3  6818  fvrn0  6850  ndmfv  6855  elfv2ex  6866  fveqres  6867  csbfv12  6868  csbfv  6870  dffv2  6918  fvco4i  6924  fvmptss  6942  fvmptex  6944  fvmptss2  6956  fvmptrabfv  6962  f0cli  7032  fvunsn  7115  fconst5  7142  csbriota  7321  riotassuni  7346  oprabidw  7380  csbov123  7393  csbov  7394  fvmptopab  7404  brfvopab  7406  elimdelov  7445  ovif12  7449  ifmpt2v  7451  ndmovcl  7534  ndmovord  7539  elovmpt3imp  7606  difsnexi  7697  ordsuc  7747  ordsucelsuc  7755  1stval  7926  2ndval  7927  1st2val  7952  2nd2val  7953  el2mpocsbcl  8018  bropopvvv  8023  bropfvvvvlem  8024  bropfvvvv  8025  suppimacnv  8107  suppssdm  8110  ressuppss  8116  suppun  8117  extmptsuppeq  8121  funsssuppss  8123  fczsupp0  8126  suppss  8127  suppss2  8133  suppssfv  8135  suppco  8139  mpoxopynvov0  8151  mpoxopoveqd  8154  pwuninel  8208  smofvon2  8279  om0x  8437  mapssfset  8778  brdomg  8884  snfi  8968  snfiOLD  8969  sdomirr  9031  domunsn  9044  2pwuninel  9049  unfi  9085  cnvfi  9090  suppeqfsuppbi  9269  fsuppun  9277  funsnfsupp  9282  fipwuni  9316  oicl  9421  oif  9422  wemapso2  9445  card2on  9446  en2lp  9502  ttrclselem1  9621  tctr  9636  r1tr  9672  rankdmr1  9697  r1pw  9741  r1pwALT  9742  rankuni  9759  scottex  9781  cardidm  9855  alephcard  9964  alephnbtwn  9965  cfub  10143  cardcf  10146  cflecard  10147  cfle  10148  cflim2  10157  cfidm  10169  isf32lem9  10255  itunisuc  10313  itunitc1  10314  itunitc  10315  ituniiun  10316  axcc2lem  10330  alephreg  10476  pwcfsdom  10477  cfpwsdom  10478  axunndlem1  10489  axpownd  10495  tskmcl  10735  addcompi  10788  addasspi  10789  mulcompi  10790  mulasspi  10791  distrpi  10792  addnidpi  10795  nlt1pi  10800  addcompq  10844  addcomnq  10845  mulcompq  10846  mulcomnq  10847  adderpq  10850  mulerpq  10851  addassnq  10852  mulassnq  10853  distrnq  10855  genpass  10903  addcompr  10915  mulcompr  10917  distrpr  10922  ltexprlem7  10936  addcomsr  10981  addasssr  10982  mulcomsr  10983  mulasssr  10984  distrsr  10985  uzssz  12756  uzwo  12812  nn01to3  12842  xnn0xaddcl  13137  elixx3g  13261  iooid  13276  elfz2  13417  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  14489  swrd00  14551  swrd0  14565  swrdwrdsymb  14569  pfx00  14581  pfx0  14582  repswswrd  14690  0csh0  14699  cshwcl  14704  cshwidxmod  14709  repswcshw  14718  cshw1  14728  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  18520  grpidval  18535  gsum0  18558  frmdplusg  18728  frmd0  18734  efmndbas  18745  efmndbasabf  18746  efmndplusg  18754  mgm2nsgrplem2  18793  mgm2nsgrplem3  18794  sgrp2rid2  18800  dfgrp2e  18842  grpinvfval  18857  grpinvfvalALT  18858  grpinvfvi  18861  grpsubfval  18862  grpsubfvalALT  18863  mulgfval  18948  mulgfvalALT  18949  mulgfvi  18952  cntrval  19198  oppgval  19226  oppgplusfval  19227  symgval  19250  snsymgefmndeq  19274  psgnfval  19379  odfval  19411  odfvalALT  19412  oppglsm  19521  efgval  19596  mgpval  20028  mgpplusg  20029  ringidval  20068  opprval  20223  opprmulfval  20224  dvdsrval  20246  invrfval  20274  dvrfval  20287  rrgval  20582  staffval  20726  scaffval  20783  rlmval  21095  rlmsca2  21103  2idlval  21158  nzerooringczr  21387  zrhval  21414  zlmlem  21423  zlmvsca  21428  chrval  21430  evpmss  21493  psgndiflemB  21507  ipffval  21555  thlbas  21603  thlle  21604  thloc  21606  pjfval  21613  dsmmval2  21643  asclfval  21786  psrplusg  21843  psrmulr  21849  psrvscafval  21855  mplval  21896  mplcoe3  21943  evlval  22000  psr1val  22068  vr1val  22074  ply1val  22076  ply1basfvi  22123  ply1plusgfvi  22124  psr1sca2  22133  ply1sca2  22136  ply1ascl  22142  cply1mul  22181  gsummoncoe1  22193  evl1fval  22213  evl1fval1  22216  mamufacex  22281  mavmulsolcl  22436  marrepfval  22445  marepvfval  22450  submafval  22464  mdetfval  22471  mdetfval1  22475  mdetunilem7  22503  mdetunilem8  22504  madufval  22522  minmar1fval  22531  mp2pm2mplem4  22694  toponsspwpw  22807  tgdif0  22877  indislem  22885  resstopn  23071  iocpnfordt  23100  icomnfordt  23101  hmeofval  23643  ussval  24145  nmfval  24474  nghmfval  24608  pcofval  24908  tcphval  25116  ioombl  25464  ibladdlem  25719  itgaddlem1  25722  iblabs  25728  dvbsss  25801  perfdvf  25802  mdegfval  25965  deg1fval  25983  deg1fvi  25988  uc1pval  26043  mon1pval  26045  2irrexpq  26638  lgsqrmodndvds  27262  gausslemma2dlem1a  27274  2lgs  27316  2sqreultblem  27357  2sqreunnltblem  27360  newval  27765  leftval  27773  rightval  27774  lltropt  27786  oldssmade  27791  oldss  27792  lrold  27811  ttglem  28821  axcontlem12  28920  vtxval  28945  iedgval  28946  edgval  28994  usgr1v  29201  nbuhgr  29288  nbumgr  29292  uhgrnbgr0nb  29299  nbgr1vtx  29303  nbgrnself2  29305  nbusgrvtxm1  29324  sizusglecusg  29409  g0wlk0  29596  wlkreslem  29613  lfgrwlkprop  29631  wwlks  29780  wwlksn  29782  wspthsn  29793  iswwlksnon  29798  iswspthsnon  29801  0enwwlksnge1  29809  wwlksnfi  29851  clwwlk  29927  umgrclwwlkge2  29935  clwlkclwwlklem2a4  29941  clwwlkn  29970  clwwlknonmpo  30033  clwwlknon  30034  clwwlk0on0  30036  clwwlknon1le1  30045  1conngr  30138  eupth2lem3lem7  30178  frgr1v  30215  nfrgr2v  30216  1to2vfriswmgr  30223  2wspmdisj  30281  frgrreggt1  30337  frgrreg  30338  frgrregord013  30339  frgrogt3nreg  30341  friendship  30343  avril1  30407  vafval  30547  bafval  30548  smfval  30549  vsfval  30577  bcsiALT  31123  of0r  32621  fracval  33243  fracbas  33244  resvsca  33270  resvlem  33271  cntnevol  34195  signsw0glem  34521  bnj1189  34976  fmlafvel  35358  gonan0  35365  satffun  35382  mvtval  35473  mexval  35475  mexval2  35476  mdvval  35477  mrsubfval  35481  mrsubrn  35486  msubfval  35497  elmsubrn  35501  msubrn  35502  mvhfval  35506  mpstval  35508  msrfval  35510  mstaval  35517  mppsval  35545  mthmval  35548  antnestlaw2  35665  dfrdg3  35770  fvsingle  35894  unisnif  35899  funpartfv  35919  fullfunfv  35921  linedegen  36117  bj-ax6e  36642  axc11n11r  36657  bj-ax12v3ALT  36660  bj-sbsb  36811  bj-nfcsym  36873  bj-snex  37009  bj-restsnid  37061  bj-inftyexpitaudisj  37179  bj-inftyexpidisj  37184  finxpreclem4  37368  finxp00  37376  isinf2  37379  wl-nfs1t  37511  matunitlindflem1  37596  itg2addnclem  37651  ibladdnclem  37656  itgaddnclem1  37658  iblabsnc  37664  iblmulc2nc  37665  ftc1anclem8  37680  ismgmOLD  37830  tsbi1  38113  tsbi2  38114  ac6s6  38152  equid1  38878  ax12fromc15  38884  equid1ALT  38904  dvelimf-o  38908  ax12inda2ALT  38925  ax12inda2  38926  sn-axprlem3  42190  fsuppind  42563  mzpmfp  42720  itgocn  43137  mendbas  43153  mendplusgfval  43154  mendmulrfval  43156  mendsca  43158  mendvscafval  43159  arearect  43188  areaquad  43189  fpwfvss  43385  safesnsupfidom1o  43390  sn1dom  43499  or3or  43996  uneqsn  43998  addcomgi  44429  ax6e2ndeq  44533  2sb5ndVD  44883  2sb5ndALT  44905  sqwvfoura  46209  sqwvfourb  46210  fourierswlem  46211  fouriersw  46212  hspdifhsp  46597  hspmbllem2  46608  hspmbl  46610  et-ltneverrefl  46852  tz6.12-afv  47157  ndmaovcl  47187  tz6.12-afv2  47224  otiunsndisjX  47263  fvmptrab  47276  nltle2tri  47297  fzopredsuc  47307  iccpartiltu  47406  iccpartigtl  47407  iccpartlt  47408  icceuelpartlem  47419  iccpartnel  47422  elsprel  47459  sprssspr  47465  sprsymrelfvlem  47474  prprelprb  47501  prprspr2  47502  fmtnoprmfac1  47549  fmtnoprmfac2  47551  prmdvdsfmtnof1lem2  47569  prminf2  47572  lighneallem4  47594  requad1  47606  requad2  47607  evenprm2  47698  even3prm2  47703  fpprbasnn  47713  stgoldbwt  47760  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem2lem3  48100  upwlkbprop  48122  pgrpgt2nabl  48350  suppmptcfin  48360  linc1  48410  lindslinindsimp2lem5  48447  1aryenef  48630  2aryenef  48641  reorelicc  48695  rrxsphere  48733  fvconst0ci  48875  fvconstdomi  48876  upfval  49161  reldmprcof1  49366  reldmprcof2  49367  lmdfval  49634  cmdfval  49635  setrec2lem1  49678  setrec2mpt  49682