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  2382  ax12  2422  exdistrf  2446  equvini  2454  ax12vALT  2468  2ax6e  2470  sb1  2477  sb2  2478  sb4a  2479  dfsb1  2480  dfsb2  2492  sbcom3  2505  sbco2  2510  sbco3  2512  sb9  2518  eujustALT  2566  pm2.61ine  3009  ralcom2  3353  eueq2  3684  moeq3  3686  mo2icl  3688  sbc2or  3765  unineq  4254  csb0  4376  sbcel12  4377  sbcne12  4381  sbcel2  4384  csbidm  4399  csbun  4407  csbin  4408  csbdif  4490  ifsb  4505  ifid  4532  ifnot  4544  ifan  4545  ifor  4546  csbif  4549  elimhyp  4557  elimhyp2v  4558  elimhyp3v  4559  elimhyp4v  4560  elimdhyp  4562  keephyp2v  4564  keephyp3v  4565  rmosn  4686  rabsnif  4690  tppreqb  4772  ssunsn2  4794  n0snor2el  4800  preq12nebg  4830  opthprneg  4832  elpreqprlem  4833  dfopif  4837  csbuni  4903  disjord  5099  sbcbr  5165  unisn2  5270  intabs  5307  class2set  5313  dtruALT2  5328  snexALT  5341  dtruALT  5346  axprlem3  5383  axprlem3OLD  5386  snex  5394  exneq  5398  dtruOLD  5404  copsexgw  5453  copsexg  5454  snopeqop  5469  csbopab  5518  dfid3  5539  csbxp  5741  csbres  5956  csbima12  6053  soirri  6102  csbrn  6179  dmsnopss  6190  dmsnsnsn  6196  opswap  6205  unixpid  6260  predres  6315  nsuceq0  6420  ordsssuc2  6428  iotassuni  6486  iotaex  6487  iotassuniOLD  6493  iotaexOLD  6494  csbiota  6507  dffv3  6857  fvrn0  6891  ndmfv  6896  elfv2ex  6907  fveqres  6908  csbfv12  6909  csbfv  6911  dffv2  6959  fvco4i  6965  fvmptss  6983  fvmptex  6985  fvmptss2  6997  fvmptrabfv  7003  f0cli  7073  fvunsn  7156  fconst5  7183  csbriota  7362  riotassuni  7387  oprabidw  7421  csbov123  7434  csbov  7435  fvmptopab  7446  fvmptopabOLD  7447  brfvopab  7449  elimdelov  7488  ovif12  7492  ifmpt2v  7494  ndmovcl  7577  ndmovord  7582  elovmpt3imp  7649  difsnexi  7740  ordsuc  7791  ordsucOLD  7792  ordsucelsuc  7800  1stval  7973  2ndval  7974  1st2val  7999  2nd2val  8000  el2mpocsbcl  8067  bropopvvv  8072  bropfvvvvlem  8073  bropfvvvv  8074  suppimacnv  8156  suppssdm  8159  ressuppss  8165  suppun  8166  extmptsuppeq  8170  funsssuppss  8172  fczsupp0  8175  suppss  8176  suppss2  8182  suppssfv  8184  suppco  8188  mpoxopynvov0  8200  mpoxopoveqd  8203  pwuninel  8257  smofvon2  8328  om0x  8486  mapssfset  8827  brdomg  8933  snfi  9017  snfiOLD  9018  sdomirr  9084  domunsn  9097  2pwuninel  9102  unfi  9141  cnvfi  9146  suppeqfsuppbi  9337  fsuppun  9345  funsnfsupp  9350  fipwuni  9384  oicl  9489  oif  9490  wemapso2  9513  card2on  9514  en2lp  9566  ttrclselem1  9685  tctr  9700  r1tr  9736  rankdmr1  9761  r1pw  9805  r1pwALT  9806  rankuni  9823  scottex  9845  cardidm  9919  alephcard  10030  alephnbtwn  10031  cfub  10209  cardcf  10212  cflecard  10213  cfle  10214  cflim2  10223  cfidm  10235  isf32lem9  10321  itunisuc  10379  itunitc1  10380  itunitc  10381  ituniiun  10382  axcc2lem  10396  alephreg  10542  pwcfsdom  10543  cfpwsdom  10544  axunndlem1  10555  axpownd  10561  tskmcl  10801  addcompi  10854  addasspi  10855  mulcompi  10856  mulasspi  10857  distrpi  10858  addnidpi  10861  nlt1pi  10866  addcompq  10910  addcomnq  10911  mulcompq  10912  mulcomnq  10913  adderpq  10916  mulerpq  10917  addassnq  10918  mulassnq  10919  distrnq  10921  genpass  10969  addcompr  10981  mulcompr  10983  distrpr  10988  ltexprlem7  11002  addcomsr  11047  addasssr  11048  mulcomsr  11049  mulasssr  11050  distrsr  11051  uzssz  12821  uzwo  12877  nn01to3  12907  xnn0xaddcl  13202  elixx3g  13326  iooid  13341  elfz2  13482  injresinjlem  13755  injresinj  13756  fleqceilz  13823  modifeq2int  13905  modfzo0difsn  13915  addmodlteq  13918  ltweuz  13933  fzofi  13946  fsuppmapnn0fiubex  13964  hashrabrsn  14344  hashrabsn01  14345  hashrabsn1  14346  elprchashprn2  14368  hashss  14381  hashsn01  14388  hash1snb  14391  hashgt12el  14394  hashgt12el2  14395  hashgt23el  14396  hashfzp1  14403  hashfundm  14414  hash2pwpr  14448  hashge2el2dif  14452  hash3tpde  14465  ffz0iswrd  14513  ccatsymb  14554  swrd00  14616  swrd0  14630  swrdwrdsymb  14634  pfx00  14646  pfx0  14647  repswswrd  14756  0csh0  14765  cshwcl  14770  cshwidxmod  14775  repswcshw  14784  cshw1  14794  s3sndisj  14940  s3iunsndisj  14941  xptrrel  14953  trclfvcotrg  14989  relexpfld  15022  reusq0  15438  modfsummods  15766  dvdsaddre2b  16284  gcdaddmlem  16501  prm23ge5  16793  pcmptcl  16869  prmgaplem5  17033  prmgaplem6  17034  cshwshash  17082  strle1  17135  strfvss  17164  strfvi  17167  setsnid  17185  ressbas  17213  ressbasssg  17214  ressbasssOLD  17217  resseqnbas  17219  ress0  17220  ressress  17224  0rest  17399  firest  17402  topnval  17404  xpsaddlem  17543  xpsvsca  17547  homffval  17658  comfffval  17666  oppchomfval  17682  oppcbas  17686  fullfunc  17877  fthfunc  17878  natfval  17918  fucbas  17932  fuchom  17933  arwval  18012  coafval  18033  xpcbas  18146  xpchomfval  18147  xpccofval  18150  oduval  18256  oduleval  18257  lubfun  18318  glbfun  18331  odujoin  18374  odumeet  18376  ipopos  18502  plusffval  18580  grpidval  18595  gsum0  18618  frmdplusg  18788  frmd0  18794  efmndbas  18805  efmndbasabf  18806  efmndplusg  18814  mgm2nsgrplem2  18853  mgm2nsgrplem3  18854  sgrp2rid2  18860  dfgrp2e  18902  grpinvfval  18917  grpinvfvalALT  18918  grpinvfvi  18921  grpsubfval  18922  grpsubfvalALT  18923  mulgfval  19008  mulgfvalALT  19009  mulgfvi  19012  cntrval  19258  oppgval  19286  oppgplusfval  19287  symgval  19308  snsymgefmndeq  19332  psgnfval  19437  odfval  19469  odfvalALT  19470  oppglsm  19579  efgval  19654  mgpval  20059  mgpplusg  20060  ringidval  20099  opprval  20254  opprmulfval  20255  dvdsrval  20277  invrfval  20305  dvrfval  20318  rrgval  20613  staffval  20757  scaffval  20793  rlmval  21105  rlmsca2  21113  2idlval  21168  nzerooringczr  21397  zrhval  21424  zlmlem  21433  zlmvsca  21438  chrval  21440  evpmss  21502  psgndiflemB  21516  ipffval  21564  thlbas  21612  thlle  21613  thloc  21615  pjfval  21622  dsmmval2  21652  asclfval  21795  psrplusg  21852  psrmulr  21858  psrvscafval  21864  mplval  21905  mplcoe3  21952  evlval  22009  psr1val  22077  vr1val  22083  ply1val  22085  ply1basfvi  22132  ply1plusgfvi  22133  psr1sca2  22142  ply1sca2  22145  ply1ascl  22151  cply1mul  22190  gsummoncoe1  22202  evl1fval  22222  evl1fval1  22225  mamufacex  22290  mavmulsolcl  22445  marrepfval  22454  marepvfval  22459  submafval  22473  mdetfval  22480  mdetfval1  22484  mdetunilem7  22512  mdetunilem8  22513  madufval  22531  minmar1fval  22540  mp2pm2mplem4  22703  toponsspwpw  22816  tgdif0  22886  indislem  22894  resstopn  23080  iocpnfordt  23109  icomnfordt  23110  hmeofval  23652  ussval  24154  nmfval  24483  nghmfval  24617  pcofval  24917  tcphval  25125  ioombl  25473  ibladdlem  25728  itgaddlem1  25731  iblabs  25737  dvbsss  25810  perfdvf  25811  mdegfval  25974  deg1fval  25992  deg1fvi  25997  uc1pval  26052  mon1pval  26054  2irrexpq  26647  lgsqrmodndvds  27271  gausslemma2dlem1a  27283  2lgs  27325  2sqreultblem  27366  2sqreunnltblem  27369  newval  27770  leftval  27778  rightval  27779  lltropt  27791  oldssmade  27796  lrold  27815  ttglem  28810  axcontlem12  28909  vtxval  28934  iedgval  28935  edgval  28983  usgr1v  29190  nbuhgr  29277  nbumgr  29281  uhgrnbgr0nb  29288  nbgr1vtx  29292  nbgrnself2  29294  nbusgrvtxm1  29313  sizusglecusg  29398  g0wlk0  29587  wlkreslem  29604  lfgrwlkprop  29622  wwlks  29772  wwlksn  29774  wspthsn  29785  iswwlksnon  29790  iswspthsnon  29793  0enwwlksnge1  29801  wwlksnfi  29843  clwwlk  29919  umgrclwwlkge2  29927  clwlkclwwlklem2a4  29933  clwwlkn  29962  clwwlknonmpo  30025  clwwlknon  30026  clwwlk0on0  30028  clwwlknon1le1  30037  1conngr  30130  eupth2lem3lem7  30170  frgr1v  30207  nfrgr2v  30208  1to2vfriswmgr  30215  2wspmdisj  30273  frgrreggt1  30329  frgrreg  30330  frgrregord013  30331  frgrogt3nreg  30333  friendship  30335  avril1  30399  vafval  30539  bafval  30540  smfval  30541  vsfval  30569  bcsiALT  31115  of0r  32609  fracval  33261  fracbas  33262  resvsca  33311  resvlem  33312  cntnevol  34225  signsw0glem  34551  bnj1189  35006  fmlafvel  35379  gonan0  35386  satffun  35403  mvtval  35494  mexval  35496  mexval2  35497  mdvval  35498  mrsubfval  35502  mrsubrn  35507  msubfval  35518  elmsubrn  35522  msubrn  35523  mvhfval  35527  mpstval  35529  msrfval  35531  mstaval  35538  mppsval  35566  mthmval  35569  antnestlaw2  35686  dfrdg3  35791  fvsingle  35915  unisnif  35920  funpartfv  35940  fullfunfv  35942  linedegen  36138  bj-ax6e  36663  axc11n11r  36678  bj-ax12v3ALT  36681  bj-sbsb  36832  bj-nfcsym  36894  bj-snex  37030  bj-restsnid  37082  bj-inftyexpitaudisj  37200  bj-inftyexpidisj  37205  finxpreclem4  37389  finxp00  37397  isinf2  37400  wl-nfs1t  37532  matunitlindflem1  37617  itg2addnclem  37672  ibladdnclem  37677  itgaddnclem1  37679  iblabsnc  37685  iblmulc2nc  37686  ftc1anclem8  37701  ismgmOLD  37851  tsbi1  38134  tsbi2  38135  ac6s6  38173  equid1  38899  ax12fromc15  38905  equid1ALT  38925  dvelimf-o  38929  ax12inda2ALT  38946  ax12inda2  38947  sn-axprlem3  42212  fsuppind  42585  mzpmfp  42742  itgocn  43160  mendbas  43176  mendplusgfval  43177  mendmulrfval  43179  mendsca  43181  mendvscafval  43182  arearect  43211  areaquad  43212  fpwfvss  43408  safesnsupfidom1o  43413  sn1dom  43522  or3or  44019  uneqsn  44021  addcomgi  44452  ax6e2ndeq  44556  2sb5ndVD  44906  2sb5ndALT  44928  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  hspdifhsp  46621  hspmbllem2  46632  hspmbl  46634  et-ltneverrefl  46876  tz6.12-afv  47178  ndmaovcl  47208  tz6.12-afv2  47245  otiunsndisjX  47284  fvmptrab  47297  nltle2tri  47318  fzopredsuc  47328  iccpartiltu  47427  iccpartigtl  47428  iccpartlt  47429  icceuelpartlem  47440  iccpartnel  47443  elsprel  47480  sprssspr  47486  sprsymrelfvlem  47495  prprelprb  47522  prprspr2  47523  fmtnoprmfac1  47570  fmtnoprmfac2  47572  prmdvdsfmtnof1lem2  47590  prminf2  47593  lighneallem4  47615  requad1  47627  requad2  47628  evenprm2  47719  even3prm2  47724  fpprbasnn  47734  stgoldbwt  47781  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  upwlkbprop  48130  pgrpgt2nabl  48358  suppmptcfin  48368  linc1  48418  lindslinindsimp2lem5  48455  1aryenef  48638  2aryenef  48649  reorelicc  48703  rrxsphere  48741  fvconst0ci  48883  fvconstdomi  48884  upfval  49169  reldmprcof1  49374  reldmprcof2  49375  lmdfval  49642  cmdfval  49643  setrec2lem1  49686  setrec2mpt  49690