Theorem pm2.61i 183

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  184  pm2.61nii  185  pm2.61iii  186  pm2.65i  195  pm5.21nii  379  pm5.18  382  biass  385  pm2.61ian  817  ecase3  1038  4cases  1046  pm4.42  1059  ifpid  1082  elimh  1088  3ecase  1482  norass  1544  ax6e  2391  ax12  2431  exdistrf  2455  equvini  2463  ax12vALT  2477  2ax6e  2479  sb1  2486  sb2  2487  sb4a  2488  dfsb1  2489  dfsb2  2501  sbcom3  2514  sbco2  2519  sbco3  2521  sb9  2527  eujustALT  2576  pm2.61ine  3017  ralcom2  3341  eueq2  3651  moeq3  3653  mo2icl  3655  sbc2or  3732  unineq  4216  csb0  4338  sbcel12  4339  sbcne12  4343  sbcel2  4346  csbidm  4361  csbun  4369  csbin  4370  csbdif  4453  ifsb  4468  ifid  4495  ifnot  4507  ifan  4508  ifor  4509  csbif  4512  elimhyp  4520  elimhyp2v  4521  elimhyp3v  4522  elimhyp4v  4523  elimdhyp  4525  keephyp2v  4527  keephyp3v  4528  rmosn  4651  rabsnif  4655  tppreqb  4738  ssunsn2  4758  n0snor2el  4764  preq12nebg  4794  opthprneg  4796  elpreqprlem  4797  dfopif  4801  csbuni  4868  disjord  5061  sbcbr  5127  unisn2  5234  intabs  5277  class2set  5283  dtruALT2  5299  snexALT  5312  dtruALT  5317  axprlem3  5354  axprlem3OLD  5358  axprglem  5365  axprg  5366  snexOLD  5371  exneq  5375  copsexgwOLD  5431  copsexg  5432  snopeqop  5447  csbopab  5497  dfid3  5516  csbxp  5719  csbres  5934  csbima12  6031  soirri  6076  csbrn  6154  dmsnopss  6165  dmsnsnsn  6171  opswap  6180  unixpid  6235  predres  6290  nsuceq0  6395  ordsssuc2  6403  iotassuni  6460  iotaex  6461  csbiota  6478  dffv3  6823  fvrn0  6855  ndmfv  6859  elfv2ex  6870  fveqres  6871  csbfv12  6872  csbfv  6874  dffv2  6922  fvco4i  6929  fvmptss  6948  fvmptex  6950  fvmptss2  6962  fvmptrabfv  6968  f0cli  7039  fvunsn  7123  fconst5  7150  csbriota  7328  riotassuni  7353  oprabidw  7387  csbov123  7400  csbov  7401  fvmptopab  7411  brfvopab  7413  elimdelov  7452  ovif12  7456  ifmpt2v  7458  ndmovcl  7541  ndmovord  7546  elovmpt3imp  7613  difsnexi  7704  ordsuc  7754  ordsucelsuc  7762  1stval  7933  2ndval  7934  1st2val  7959  2nd2val  7960  el2mpocsbcl  8024  bropopvvv  8029  bropfvvvvlem  8030  bropfvvvv  8031  suppimacnv  8114  suppssdm  8117  ressuppss  8123  suppun  8124  extmptsuppeq  8128  funsssuppss  8130  fczsupp0  8133  suppss  8134  suppss2  8140  suppssfv  8142  suppco  8146  mpoxopynvov0  8158  mpoxopoveqd  8161  pwuninel  8215  smofvon2  8286  om0x  8444  mapssfset  8788  brdomg  8895  snfi  8980  sdomirr  9042  domunsn  9055  2pwuninel  9060  unfi  9095  cnvfi  9100  suppeqfsuppbi  9282  fsuppun  9290  funsnfsupp  9295  fipwuni  9329  oicl  9434  oif  9435  wemapso2  9458  card2on  9459  en2lp  9518  ttrclselem1  9637  tctr  9650  r1tr  9691  rankdmr1  9716  r1pw  9760  r1pwALT  9761  rankuni  9778  scottex  9800  cardidm  9874  alephcard  9983  alephnbtwn  9984  cfub  10162  cardcf  10165  cflecard  10166  cfle  10167  cflim2  10176  cfidm  10188  isf32lem9  10274  itunisuc  10332  itunitc1  10333  itunitc  10334  ituniiun  10335  axcc2lem  10349  alephreg  10496  pwcfsdom  10497  cfpwsdom  10498  axunndlem1  10509  axpownd  10515  tskmcl  10755  addcompi  10808  addasspi  10809  mulcompi  10810  mulasspi  10811  distrpi  10812  addnidpi  10815  nlt1pi  10820  addcompq  10864  addcomnq  10865  mulcompq  10866  mulcomnq  10867  adderpq  10870  mulerpq  10871  addassnq  10872  mulassnq  10873  distrnq  10875  genpass  10923  addcompr  10935  mulcompr  10937  distrpr  10942  ltexprlem7  10956  addcomsr  11001  addasssr  11002  mulcomsr  11003  mulasssr  11004  distrsr  11005  indval0  12154  uzssz  12800  uzwo  12852  nn01to3  12882  xnn0xaddcl  13178  elixx3g  13302  iooid  13317  elfz2  13459  injresinjlem  13736  injresinj  13737  fleqceilz  13804  modifeq2int  13886  modfzo0difsn  13896  addmodlteq  13899  ltweuz  13914  fzofi  13927  fsuppmapnn0fiubex  13945  hashrabrsn  14325  hashrabsn01  14326  hashrabsn1  14327  elprchashprn2  14349  hashss  14362  hashsn01  14369  hash1snb  14372  hashgt12el  14375  hashgt12el2  14376  hashgt23el  14377  hashfzp1  14384  hashfundm  14395  hash2pwpr  14429  hashge2el2dif  14433  hash3tpde  14446  ffz0iswrd  14494  ccatsymb  14536  swrd00  14598  swrd0  14612  swrdwrdsymb  14616  pfx00  14628  pfx0  14629  repswswrd  14737  0csh0  14746  cshwcl  14751  cshwidxmod  14756  repswcshw  14765  cshw1  14775  s3sndisj  14920  s3iunsndisj  14921  xptrrel  14933  trclfvcotrg  14969  relexpfld  15002  reusq0  15418  modfsummods  15747  dvdsaddre2b  16267  gcdaddmlem  16484  prm23ge5  16777  pcmptcl  16853  prmgaplem5  17017  prmgaplem6  17018  cshwshash  17066  strle1  17119  strfvss  17148  strfvi  17151  setsnid  17169  ressbas  17197  ressbasssg  17198  ressbasssOLD  17201  resseqnbas  17203  ress0  17204  ressress  17208  0rest  17383  firest  17386  topnval  17388  xpsaddlem  17528  xpsvsca  17532  homffval  17647  comfffval  17655  oppchomfval  17671  oppcbas  17675  fullfunc  17866  fthfunc  17867  natfval  17907  fucbas  17921  fuchom  17922  arwval  18001  coafval  18022  xpcbas  18135  xpchomfval  18136  xpccofval  18139  oduval  18245  oduleval  18246  lubfun  18307  glbfun  18320  odujoin  18363  odumeet  18365  ipopos  18493  plusffval  18605  grpidval  18620  gsum0  18643  frmdplusg  18813  frmd0  18819  efmndbas  18830  efmndbasabf  18831  efmndplusg  18839  mgm2nsgrplem2  18881  mgm2nsgrplem3  18882  sgrp2rid2  18888  dfgrp2e  18930  grpinvfval  18945  grpinvfvalALT  18946  grpinvfvi  18949  grpsubfval  18950  grpsubfvalALT  18951  mulgfval  19036  mulgfvalALT  19037  mulgfvi  19040  cntrval  19285  oppgval  19313  oppgplusfval  19314  symgval  19337  snsymgefmndeq  19361  psgnfval  19466  odfval  19498  odfvalALT  19499  oppglsm  19608  efgval  19683  mgpval  20115  mgpplusg  20116  ringidval  20155  opprval  20309  opprmulfval  20310  dvdsrval  20332  invrfval  20360  dvrfval  20373  rrgval  20669  staffval  20813  scaffval  20870  rlmval  21181  rlmsca2  21189  2idlval  21244  nzerooringczr  21455  zrhval  21482  zlmlem  21491  zlmvsca  21496  chrval  21498  evpmss  21561  psgndiflemB  21575  ipffval  21623  thlbas  21671  thlle  21672  thloc  21674  pjfval  21681  dsmmval2  21711  asclfval  21853  psrplusg  21912  psrmulr  21917  psrvscafval  21923  mplval  21963  mplcoe3  22014  evlval  22076  psr1val  22171  vr1val  22177  ply1val  22179  ply1basfvi  22225  ply1plusgfvi  22226  psr1sca2  22235  ply1sca2  22238  ply1ascl  22244  cply1mul  22282  gsummoncoe1  22294  evl1fval  22314  evl1fval1  22317  mamufacex  22379  mavmulsolcl  22534  marrepfval  22543  marepvfval  22548  submafval  22562  mdetfval  22569  mdetfval1  22573  mdetunilem7  22601  mdetunilem8  22602  madufval  22620  minmar1fval  22629  mp2pm2mplem4  22792  toponsspwpw  22905  tgdif0  22975  indislem  22983  resstopn  23169  iocpnfordt  23198  icomnfordt  23199  hmeofval  23741  ussval  24242  nmfval  24571  nghmfval  24705  pcofval  24995  tcphval  25203  ioombl  25550  ibladdlem  25805  itgaddlem1  25808  iblabs  25814  dvbsss  25887  perfdvf  25888  mdegfval  26045  deg1fval  26063  deg1fvi  26068  uc1pval  26123  mon1pval  26125  2irrexpq  26713  lgsqrmodndvds  27334  gausslemma2dlem1a  27346  2lgs  27388  2sqreultblem  27429  2sqreunnltblem  27432  newval  27845  leftval  27859  rightval  27860  lltr  27872  oldssmade  27877  oldss  27880  lrold  27907  ttglem  28962  axcontlem12  29062  vtxval  29087  iedgval  29088  edgval  29136  usgr1v  29343  nbuhgr  29430  nbumgr  29434  uhgrnbgr0nb  29441  nbgr1vtx  29445  nbgrnself2  29447  nbusgrvtxm1  29466  sizusglecusg  29550  g0wlk0  29737  wlkreslem  29754  lfgrwlkprop  29772  wwlks  29921  wwlksn  29923  wspthsn  29934  iswwlksnon  29939  iswspthsnon  29942  0enwwlksnge1  29950  wwlksnfi  29992  clwwlk  30071  umgrclwwlkge2  30079  clwlkclwwlklem2a4  30085  clwwlkn  30114  clwwlknonmpo  30177  clwwlknon  30178  clwwlk0on0  30180  clwwlknon1le1  30189  1conngr  30282  eupth2lem3lem7  30322  frgr1v  30359  nfrgr2v  30360  1to2vfriswmgr  30367  2wspmdisj  30425  frgrreggt1  30481  frgrreg  30482  frgrregord013  30483  frgrogt3nreg  30485  friendship  30487  avril1  30551  vafval  30692  bafval  30693  smfval  30694  vsfval  30722  bcsiALT  31268  of0r  32771  fracval  33388  fracbas  33389  resvsca  33415  resvlem  33416  cntnevol  34412  signsw0glem  34737  bnj1189  35191  r1wf  35277  noinfepregs  35314  fmlafvel  35613  gonan0  35620  satffun  35637  mvtval  35728  mexval  35730  mexval2  35731  mdvval  35732  mrsubfval  35736  mrsubrn  35741  msubfval  35752  elmsubrn  35756  msubrn  35757  mvhfval  35761  mpstval  35763  msrfval  35765  mstaval  35772  mppsval  35800  mthmval  35803  antnestlaw2  35920  dfrdg3  36022  fvsingle  36146  unisnif  36151  funpartfv  36173  fullfunfv  36175  linedegen  36371  axtcond  36706  csbttc  36737  mh-setindnd  36765  bj-ax6e  37008  axc11n11r  37026  bj-ax12v3ALT  37029  bj-sbsb  37190  bj-nfcsym  37252  bj-snex  37388  bj-restsnid  37445  bj-inftyexpitaudisj  37565  bj-inftyexpidisj  37570  finxpreclem4  37756  finxp00  37764  isinf2  37767  wl-nfs1t  37908  matunitlindflem1  37983  itg2addnclem  38038  ibladdnclem  38043  itgaddnclem1  38045  iblabsnc  38051  iblmulc2nc  38052  ftc1anclem8  38067  ismgmOLD  38217  tsbi1  38500  tsbi2  38501  ac6s6  38539  equid1  39391  ax12fromc15  39397  equid1ALT  39417  dvelimf-o  39421  ax12inda2ALT  39438  ax12inda2  39439  sn-axprlem3  42705  fsuppind  43040  mzpmfp  43196  itgocn  43609  mendbas  43625  mendplusgfval  43626  mendmulrfval  43628  mendsca  43630  mendvscafval  43631  arearect  43660  areaquad  43661  fpwfvss  43856  safesnsupfidom1o  43861  sn1dom  43970  or3or  44467  uneqsn  44469  addcomgi  44899  ax6e2ndeq  45003  2sb5ndVD  45353  2sb5ndALT  45375  sqwvfoura  46671  sqwvfourb  46672  fourierswlem  46673  fouriersw  46674  hspdifhsp  47059  hspmbllem2  47070  hspmbl  47072  et-ltneverrefl  47314  tz6.12-afv  47636  ndmaovcl  47666  tz6.12-afv2  47703  otiunsndisjX  47742  fvmptrab  47755  nltle2tri  47776  fzopredsuc  47787  iccpartiltu  47897  iccpartigtl  47898  iccpartlt  47899  icceuelpartlem  47910  iccpartnel  47913  elsprel  47950  sprssspr  47956  sprsymrelfvlem  47965  prprelprb  47992  prprspr2  47993  fmtnoprmfac1  48043  fmtnoprmfac2  48045  prmdvdsfmtnof1lem2  48063  prminf2  48066  lighneallem4  48088  requad1  48113  requad2  48114  evenprm2  48205  even3prm2  48210  fpprbasnn  48220  stgoldbwt  48267  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  upwlkbprop  48629  pgrpgt2nabl  48857  suppmptcfin  48867  linc1  48916  lindslinindsimp2lem5  48953  1aryenef  49136  2aryenef  49147  reorelicc  49201  rrxsphere  49239  fvconst0ci  49381  fvconstdomi  49382  upfval  49666  reldmprcof1  49871  reldmprcof2  49872  lmdfval  50139  cmdfval  50140  setrec2lem1  50183  setrec2mpt  50187