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  3351  eueq2  3681  moeq3  3683  mo2icl  3685  sbc2or  3762  unineq  4251  csb0  4373  sbcel12  4374  sbcne12  4378  sbcel2  4381  csbidm  4396  csbun  4404  csbin  4405  csbdif  4487  ifsb  4502  ifid  4529  ifnot  4541  ifan  4542  ifor  4543  csbif  4546  elimhyp  4554  elimhyp2v  4555  elimhyp3v  4556  elimhyp4v  4557  elimdhyp  4559  keephyp2v  4561  keephyp3v  4562  rmosn  4683  rabsnif  4687  tppreqb  4769  ssunsn2  4791  n0snor2el  4797  preq12nebg  4827  opthprneg  4829  elpreqprlem  4830  dfopif  4834  csbuni  4900  disjord  5096  sbcbr  5162  unisn2  5267  intabs  5304  class2set  5310  dtruALT2  5325  snexALT  5338  dtruALT  5343  axprlem3  5380  axprlem3OLD  5383  snex  5391  exneq  5395  dtruOLD  5401  copsexgw  5450  copsexg  5451  snopeqop  5466  csbopab  5515  dfid3  5536  csbxp  5738  csbres  5953  csbima12  6050  soirri  6099  csbrn  6176  dmsnopss  6187  dmsnsnsn  6193  opswap  6202  unixpid  6257  predres  6312  nsuceq0  6417  ordsssuc2  6425  iotassuni  6483  iotaex  6484  iotassuniOLD  6490  iotaexOLD  6491  csbiota  6504  dffv3  6854  fvrn0  6888  ndmfv  6893  elfv2ex  6904  fveqres  6905  csbfv12  6906  csbfv  6908  dffv2  6956  fvco4i  6962  fvmptss  6980  fvmptex  6982  fvmptss2  6994  fvmptrabfv  7000  f0cli  7070  fvunsn  7153  fconst5  7180  csbriota  7359  riotassuni  7384  oprabidw  7418  csbov123  7431  csbov  7432  fvmptopab  7443  fvmptopabOLD  7444  brfvopab  7446  elimdelov  7485  ovif12  7489  ifmpt2v  7491  ndmovcl  7574  ndmovord  7579  elovmpt3imp  7646  difsnexi  7737  ordsuc  7788  ordsucOLD  7789  ordsucelsuc  7797  1stval  7970  2ndval  7971  1st2val  7996  2nd2val  7997  el2mpocsbcl  8064  bropopvvv  8069  bropfvvvvlem  8070  bropfvvvv  8071  suppimacnv  8153  suppssdm  8156  ressuppss  8162  suppun  8163  extmptsuppeq  8167  funsssuppss  8169  fczsupp0  8172  suppss  8173  suppss2  8179  suppssfv  8181  suppco  8185  mpoxopynvov0  8197  mpoxopoveqd  8200  pwuninel  8254  smofvon2  8325  om0x  8483  mapssfset  8824  brdomg  8930  snfi  9014  snfiOLD  9015  sdomirr  9078  domunsn  9091  2pwuninel  9096  unfi  9135  cnvfi  9140  suppeqfsuppbi  9330  fsuppun  9338  funsnfsupp  9343  fipwuni  9377  oicl  9482  oif  9483  wemapso2  9506  card2on  9507  en2lp  9559  ttrclselem1  9678  tctr  9693  r1tr  9729  rankdmr1  9754  r1pw  9798  r1pwALT  9799  rankuni  9816  scottex  9838  cardidm  9912  alephcard  10023  alephnbtwn  10024  cfub  10202  cardcf  10205  cflecard  10206  cfle  10207  cflim2  10216  cfidm  10228  isf32lem9  10314  itunisuc  10372  itunitc1  10373  itunitc  10374  ituniiun  10375  axcc2lem  10389  alephreg  10535  pwcfsdom  10536  cfpwsdom  10537  axunndlem1  10548  axpownd  10554  tskmcl  10794  addcompi  10847  addasspi  10848  mulcompi  10849  mulasspi  10850  distrpi  10851  addnidpi  10854  nlt1pi  10859  addcompq  10903  addcomnq  10904  mulcompq  10905  mulcomnq  10906  adderpq  10909  mulerpq  10910  addassnq  10911  mulassnq  10912  distrnq  10914  genpass  10962  addcompr  10974  mulcompr  10976  distrpr  10981  ltexprlem7  10995  addcomsr  11040  addasssr  11041  mulcomsr  11042  mulasssr  11043  distrsr  11044  uzssz  12814  uzwo  12870  nn01to3  12900  xnn0xaddcl  13195  elixx3g  13319  iooid  13334  elfz2  13475  injresinjlem  13748  injresinj  13749  fleqceilz  13816  modifeq2int  13898  modfzo0difsn  13908  addmodlteq  13911  ltweuz  13926  fzofi  13939  fsuppmapnn0fiubex  13957  hashrabrsn  14337  hashrabsn01  14338  hashrabsn1  14339  elprchashprn2  14361  hashss  14374  hashsn01  14381  hash1snb  14384  hashgt12el  14387  hashgt12el2  14388  hashgt23el  14389  hashfzp1  14396  hashfundm  14407  hash2pwpr  14441  hashge2el2dif  14445  hash3tpde  14458  ffz0iswrd  14506  ccatsymb  14547  swrd00  14609  swrd0  14623  swrdwrdsymb  14627  pfx00  14639  pfx0  14640  repswswrd  14749  0csh0  14758  cshwcl  14763  cshwidxmod  14768  repswcshw  14777  cshw1  14787  s3sndisj  14933  s3iunsndisj  14934  xptrrel  14946  trclfvcotrg  14982  relexpfld  15015  reusq0  15431  modfsummods  15759  dvdsaddre2b  16277  gcdaddmlem  16494  prm23ge5  16786  pcmptcl  16862  prmgaplem5  17026  prmgaplem6  17027  cshwshash  17075  strle1  17128  strfvss  17157  strfvi  17160  setsnid  17178  ressbas  17206  ressbasssg  17207  ressbasssOLD  17210  resseqnbas  17212  ress0  17213  ressress  17217  0rest  17392  firest  17395  topnval  17397  xpsaddlem  17536  xpsvsca  17540  homffval  17651  comfffval  17659  oppchomfval  17675  oppcbas  17679  fullfunc  17870  fthfunc  17871  natfval  17911  fucbas  17925  fuchom  17926  arwval  18005  coafval  18026  xpcbas  18139  xpchomfval  18140  xpccofval  18143  oduval  18249  oduleval  18250  lubfun  18311  glbfun  18324  odujoin  18367  odumeet  18369  ipopos  18495  plusffval  18573  grpidval  18588  gsum0  18611  frmdplusg  18781  frmd0  18787  efmndbas  18798  efmndbasabf  18799  efmndplusg  18807  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  sgrp2rid2  18853  dfgrp2e  18895  grpinvfval  18910  grpinvfvalALT  18911  grpinvfvi  18914  grpsubfval  18915  grpsubfvalALT  18916  mulgfval  19001  mulgfvalALT  19002  mulgfvi  19005  cntrval  19251  oppgval  19279  oppgplusfval  19280  symgval  19301  snsymgefmndeq  19325  psgnfval  19430  odfval  19462  odfvalALT  19463  oppglsm  19572  efgval  19647  mgpval  20052  mgpplusg  20053  ringidval  20092  opprval  20247  opprmulfval  20248  dvdsrval  20270  invrfval  20298  dvrfval  20311  rrgval  20606  staffval  20750  scaffval  20786  rlmval  21098  rlmsca2  21106  2idlval  21161  nzerooringczr  21390  zrhval  21417  zlmlem  21426  zlmvsca  21431  chrval  21433  evpmss  21495  psgndiflemB  21509  ipffval  21557  thlbas  21605  thlle  21606  thloc  21608  pjfval  21615  dsmmval2  21645  asclfval  21788  psrplusg  21845  psrmulr  21851  psrvscafval  21857  mplval  21898  mplcoe3  21945  evlval  22002  psr1val  22070  vr1val  22076  ply1val  22078  ply1basfvi  22125  ply1plusgfvi  22126  psr1sca2  22135  ply1sca2  22138  ply1ascl  22144  cply1mul  22183  gsummoncoe1  22195  evl1fval  22215  evl1fval1  22218  mamufacex  22283  mavmulsolcl  22438  marrepfval  22447  marepvfval  22452  submafval  22466  mdetfval  22473  mdetfval1  22477  mdetunilem7  22505  mdetunilem8  22506  madufval  22524  minmar1fval  22533  mp2pm2mplem4  22696  toponsspwpw  22809  tgdif0  22879  indislem  22887  resstopn  23073  iocpnfordt  23102  icomnfordt  23103  hmeofval  23645  ussval  24147  nmfval  24476  nghmfval  24610  pcofval  24910  tcphval  25118  ioombl  25466  ibladdlem  25721  itgaddlem1  25724  iblabs  25730  dvbsss  25803  perfdvf  25804  mdegfval  25967  deg1fval  25985  deg1fvi  25990  uc1pval  26045  mon1pval  26047  2irrexpq  26640  lgsqrmodndvds  27264  gausslemma2dlem1a  27276  2lgs  27318  2sqreultblem  27359  2sqreunnltblem  27362  newval  27763  leftval  27771  rightval  27772  lltropt  27784  oldssmade  27789  lrold  27808  ttglem  28803  axcontlem12  28902  vtxval  28927  iedgval  28928  edgval  28976  usgr1v  29183  nbuhgr  29270  nbumgr  29274  uhgrnbgr0nb  29281  nbgr1vtx  29285  nbgrnself2  29287  nbusgrvtxm1  29306  sizusglecusg  29391  g0wlk0  29580  wlkreslem  29597  lfgrwlkprop  29615  wwlks  29765  wwlksn  29767  wspthsn  29778  iswwlksnon  29783  iswspthsnon  29786  0enwwlksnge1  29794  wwlksnfi  29836  clwwlk  29912  umgrclwwlkge2  29920  clwlkclwwlklem2a4  29926  clwwlkn  29955  clwwlknonmpo  30018  clwwlknon  30019  clwwlk0on0  30021  clwwlknon1le1  30030  1conngr  30123  eupth2lem3lem7  30163  frgr1v  30200  nfrgr2v  30201  1to2vfriswmgr  30208  2wspmdisj  30266  frgrreggt1  30322  frgrreg  30323  frgrregord013  30324  frgrogt3nreg  30326  friendship  30328  avril1  30392  vafval  30532  bafval  30533  smfval  30534  vsfval  30562  bcsiALT  31108  of0r  32602  fracval  33254  fracbas  33255  resvsca  33304  resvlem  33305  cntnevol  34218  signsw0glem  34544  bnj1189  34999  fmlafvel  35372  gonan0  35379  satffun  35396  mvtval  35487  mexval  35489  mexval2  35490  mdvval  35491  mrsubfval  35495  mrsubrn  35500  msubfval  35511  elmsubrn  35515  msubrn  35516  mvhfval  35520  mpstval  35522  msrfval  35524  mstaval  35531  mppsval  35559  mthmval  35562  antnestlaw2  35679  dfrdg3  35784  fvsingle  35908  unisnif  35913  funpartfv  35933  fullfunfv  35935  linedegen  36131  bj-ax6e  36656  axc11n11r  36671  bj-ax12v3ALT  36674  bj-sbsb  36825  bj-nfcsym  36887  bj-snex  37023  bj-restsnid  37075  bj-inftyexpitaudisj  37193  bj-inftyexpidisj  37198  finxpreclem4  37382  finxp00  37390  isinf2  37393  wl-nfs1t  37525  matunitlindflem1  37610  itg2addnclem  37665  ibladdnclem  37670  itgaddnclem1  37672  iblabsnc  37678  iblmulc2nc  37679  ftc1anclem8  37694  ismgmOLD  37844  tsbi1  38127  tsbi2  38128  ac6s6  38166  equid1  38892  ax12fromc15  38898  equid1ALT  38918  dvelimf-o  38922  ax12inda2ALT  38939  ax12inda2  38940  sn-axprlem3  42205  fsuppind  42578  mzpmfp  42735  itgocn  43153  mendbas  43169  mendplusgfval  43170  mendmulrfval  43172  mendsca  43174  mendvscafval  43175  arearect  43204  areaquad  43205  fpwfvss  43401  safesnsupfidom1o  43406  sn1dom  43515  or3or  44012  uneqsn  44014  addcomgi  44445  ax6e2ndeq  44549  2sb5ndVD  44899  2sb5ndALT  44921  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  hspdifhsp  46614  hspmbllem2  46625  hspmbl  46627  et-ltneverrefl  46869  tz6.12-afv  47174  ndmaovcl  47204  tz6.12-afv2  47241  otiunsndisjX  47280  fvmptrab  47293  nltle2tri  47314  fzopredsuc  47324  iccpartiltu  47423  iccpartigtl  47424  iccpartlt  47425  icceuelpartlem  47436  iccpartnel  47439  elsprel  47476  sprssspr  47482  sprsymrelfvlem  47491  prprelprb  47518  prprspr2  47519  fmtnoprmfac1  47566  fmtnoprmfac2  47568  prmdvdsfmtnof1lem2  47586  prminf2  47589  lighneallem4  47611  requad1  47623  requad2  47624  evenprm2  47715  even3prm2  47720  fpprbasnn  47730  stgoldbwt  47777  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  upwlkbprop  48126  pgrpgt2nabl  48354  suppmptcfin  48364  linc1  48414  lindslinindsimp2lem5  48451  1aryenef  48634  2aryenef  48645  reorelicc  48699  rrxsphere  48737  fvconst0ci  48879  fvconstdomi  48880  upfval  49165  reldmprcof1  49370  reldmprcof2  49371  lmdfval  49638  cmdfval  49639  setrec2lem1  49682  setrec2mpt  49686