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  2387  ax12  2427  exdistrf  2451  equvini  2459  ax12vALT  2473  2ax6e  2475  sb1  2482  sb2  2483  sb4a  2484  dfsb1  2485  dfsb2  2497  sbcom3  2510  sbco2  2515  sbco3  2517  sb9  2523  eujustALT  2571  pm2.61ine  3015  ralcom2  3356  eueq2  3693  moeq3  3695  mo2icl  3697  sbc2or  3774  unineq  4263  csb0  4385  sbcel12  4386  sbcne12  4390  sbcel2  4393  csbidm  4408  csbun  4416  csbin  4417  csbdif  4499  ifsb  4514  ifid  4541  ifnot  4553  ifan  4554  ifor  4555  csbif  4558  elimhyp  4566  elimhyp2v  4567  elimhyp3v  4568  elimhyp4v  4569  elimdhyp  4571  keephyp2v  4573  keephyp3v  4574  rmosn  4695  rabsnif  4699  tppreqb  4781  ssunsn2  4803  n0snor2el  4809  preq12nebg  4839  opthprneg  4841  elpreqprlem  4842  dfopif  4846  csbuni  4912  disjord  5108  sbcbr  5174  unisn2  5282  intabs  5319  class2set  5325  dtruALT2  5340  snexALT  5353  dtruALT  5358  axprlem3  5395  axprlem3OLD  5398  snex  5406  exneq  5410  dtruOLD  5416  copsexgw  5465  copsexg  5466  snopeqop  5481  csbopab  5530  dfid3  5551  csbxp  5754  csbres  5969  csbima12  6066  soirri  6115  csbrn  6192  dmsnopss  6203  dmsnsnsn  6209  opswap  6218  unixpid  6273  predres  6328  nsuceq0  6436  ordsssuc2  6444  iotassuni  6502  iotaex  6503  iotassuniOLD  6509  iotaexOLD  6510  csbiota  6523  dffv3  6871  fvrn0  6905  ndmfv  6910  elfv2ex  6921  fveqres  6922  csbfv12  6923  csbfv  6925  dffv2  6973  fvco4i  6979  fvmptss  6997  fvmptex  6999  fvmptss2  7011  fvmptrabfv  7017  f0cli  7087  fvunsn  7170  fconst5  7197  csbriota  7375  riotassuni  7400  oprabidw  7434  csbov123  7447  csbov  7448  fvmptopab  7459  fvmptopabOLD  7460  brfvopab  7462  elimdelov  7501  ovif12  7505  ifmpt2v  7507  ndmovcl  7590  ndmovord  7595  elovmpt3imp  7662  difsnexi  7753  ordsuc  7805  ordsucOLD  7806  ordsucelsuc  7814  1stval  7988  2ndval  7989  1st2val  8014  2nd2val  8015  el2mpocsbcl  8082  bropopvvv  8087  bropfvvvvlem  8088  bropfvvvv  8089  suppimacnv  8171  suppssdm  8174  ressuppss  8180  suppun  8181  extmptsuppeq  8185  funsssuppss  8187  fczsupp0  8190  suppss  8191  suppss2  8197  suppssfv  8199  suppco  8203  mpoxopynvov0  8215  mpoxopoveqd  8218  pwuninel  8272  smofvon2  8368  om0x  8529  mapssfset  8863  brdomg  8969  brdomgOLD  8970  snfi  9055  snfiOLD  9056  sdomirr  9126  domunsn  9139  2pwuninel  9144  unfi  9183  cnvfi  9188  snnen2oOLD  9234  suppeqfsuppbi  9389  fsuppun  9397  funsnfsupp  9402  fipwuni  9436  oicl  9541  oif  9542  wemapso2  9565  card2on  9566  en2lp  9618  ttrclselem1  9737  tctr  9752  r1tr  9788  rankdmr1  9813  r1pw  9857  r1pwALT  9858  rankuni  9875  scottex  9897  cardidm  9971  alephcard  10082  alephnbtwn  10083  cfub  10261  cardcf  10264  cflecard  10265  cfle  10266  cflim2  10275  cfidm  10287  isf32lem9  10373  itunisuc  10431  itunitc1  10432  itunitc  10433  ituniiun  10434  axcc2lem  10448  alephreg  10594  pwcfsdom  10595  cfpwsdom  10596  axunndlem1  10607  axpownd  10613  tskmcl  10853  addcompi  10906  addasspi  10907  mulcompi  10908  mulasspi  10909  distrpi  10910  addnidpi  10913  nlt1pi  10918  addcompq  10962  addcomnq  10963  mulcompq  10964  mulcomnq  10965  adderpq  10968  mulerpq  10969  addassnq  10970  mulassnq  10971  distrnq  10973  genpass  11021  addcompr  11033  mulcompr  11035  distrpr  11040  ltexprlem7  11054  addcomsr  11099  addasssr  11100  mulcomsr  11101  mulasssr  11102  distrsr  11103  uzssz  12871  uzwo  12925  nn01to3  12955  xnn0xaddcl  13249  elixx3g  13373  iooid  13388  elfz2  13529  injresinjlem  13801  injresinj  13802  fleqceilz  13869  modifeq2int  13949  modfzo0difsn  13959  addmodlteq  13962  ltweuz  13977  fzofi  13990  fsuppmapnn0fiubex  14008  hashrabrsn  14388  hashrabsn01  14389  hashrabsn1  14390  elprchashprn2  14412  hashss  14425  hashsn01  14432  hash1snb  14435  hashgt12el  14438  hashgt12el2  14439  hashgt23el  14440  hashfzp1  14447  hashfundm  14458  hash2pwpr  14492  hashge2el2dif  14496  hash3tpde  14509  ffz0iswrd  14557  ccatsymb  14598  swrd00  14660  swrd0  14674  swrdwrdsymb  14678  pfx00  14690  pfx0  14691  repswswrd  14800  0csh0  14809  cshwcl  14814  cshwidxmod  14819  repswcshw  14828  cshw1  14838  s3sndisj  14984  s3iunsndisj  14985  xptrrel  14997  trclfvcotrg  15033  relexpfld  15066  reusq0  15479  modfsummods  15807  dvdsaddre2b  16324  gcdaddmlem  16541  prm23ge5  16833  pcmptcl  16909  prmgaplem5  17073  prmgaplem6  17074  cshwshash  17122  strle1  17175  strfvss  17204  strfvi  17207  setsnid  17225  ressbas  17255  ressbasssg  17256  ressbasssOLD  17259  resseqnbas  17261  ress0  17262  ressress  17266  0rest  17441  firest  17444  topnval  17446  xpsaddlem  17585  xpsvsca  17589  homffval  17700  comfffval  17708  oppchomfval  17724  oppcbas  17728  fullfunc  17919  fthfunc  17920  natfval  17960  fucbas  17974  fuchom  17975  arwval  18054  coafval  18075  xpcbas  18188  xpchomfval  18189  xpccofval  18192  oduval  18298  oduleval  18299  lubfun  18360  glbfun  18373  odujoin  18416  odumeet  18418  ipopos  18544  plusffval  18622  grpidval  18637  gsum0  18660  frmdplusg  18830  frmd0  18836  efmndbas  18847  efmndbasabf  18848  efmndplusg  18856  mgm2nsgrplem2  18895  mgm2nsgrplem3  18896  sgrp2rid2  18902  dfgrp2e  18944  grpinvfval  18959  grpinvfvalALT  18960  grpinvfvi  18963  grpsubfval  18964  grpsubfvalALT  18965  mulgfval  19050  mulgfvalALT  19051  mulgfvi  19054  cntrval  19300  oppgval  19328  oppgplusfval  19329  symgval  19350  snsymgefmndeq  19374  psgnfval  19479  odfval  19511  odfvalALT  19512  oppglsm  19621  efgval  19696  mgpval  20101  mgpplusg  20102  ringidval  20141  opprval  20296  opprmulfval  20297  dvdsrval  20319  invrfval  20347  dvrfval  20360  rrgval  20655  staffval  20799  scaffval  20835  rlmval  21147  rlmsca2  21155  2idlval  21210  nzerooringczr  21439  zrhval  21466  zlmlem  21475  zlmvsca  21480  chrval  21482  evpmss  21544  psgndiflemB  21558  ipffval  21606  thlbas  21654  thlle  21655  thloc  21657  pjfval  21664  dsmmval2  21694  asclfval  21837  psrplusg  21894  psrmulr  21900  psrvscafval  21906  mplval  21947  mplcoe3  21994  evlval  22051  psr1val  22119  vr1val  22125  ply1val  22127  ply1basfvi  22174  ply1plusgfvi  22175  psr1sca2  22184  ply1sca2  22187  ply1ascl  22193  cply1mul  22232  gsummoncoe1  22244  evl1fval  22264  evl1fval1  22267  mamufacex  22332  mavmulsolcl  22487  marrepfval  22496  marepvfval  22501  submafval  22515  mdetfval  22522  mdetfval1  22526  mdetunilem7  22554  mdetunilem8  22555  madufval  22573  minmar1fval  22582  mp2pm2mplem4  22745  toponsspwpw  22858  tgdif0  22928  indislem  22936  resstopn  23122  iocpnfordt  23151  icomnfordt  23152  hmeofval  23694  ussval  24196  nmfval  24525  nghmfval  24659  pcofval  24959  tcphval  25168  ioombl  25516  ibladdlem  25771  itgaddlem1  25774  iblabs  25780  dvbsss  25853  perfdvf  25854  mdegfval  26017  deg1fval  26035  deg1fvi  26040  uc1pval  26095  mon1pval  26097  2irrexpq  26690  lgsqrmodndvds  27314  gausslemma2dlem1a  27326  2lgs  27368  2sqreultblem  27409  2sqreunnltblem  27412  newval  27811  leftval  27819  rightval  27820  lltropt  27828  oldssmade  27833  lrold  27852  ttglem  28801  axcontlem12  28900  vtxval  28925  iedgval  28926  edgval  28974  usgr1v  29181  nbuhgr  29268  nbumgr  29272  uhgrnbgr0nb  29279  nbgr1vtx  29283  nbgrnself2  29285  nbusgrvtxm1  29304  sizusglecusg  29389  g0wlk0  29578  wlkreslem  29595  lfgrwlkprop  29613  wwlks  29763  wwlksn  29765  wspthsn  29776  iswwlksnon  29781  iswspthsnon  29784  0enwwlksnge1  29792  wwlksnfi  29834  clwwlk  29910  umgrclwwlkge2  29918  clwlkclwwlklem2a4  29924  clwwlkn  29953  clwwlknonmpo  30016  clwwlknon  30017  clwwlk0on0  30019  clwwlknon1le1  30028  1conngr  30121  eupth2lem3lem7  30161  frgr1v  30198  nfrgr2v  30199  1to2vfriswmgr  30206  2wspmdisj  30264  frgrreggt1  30320  frgrreg  30321  frgrregord013  30322  frgrogt3nreg  30324  friendship  30326  avril1  30390  vafval  30530  bafval  30531  smfval  30532  vsfval  30560  bcsiALT  31106  of0r  32602  fracval  33244  fracbas  33245  resvsca  33294  resvlem  33295  cntnevol  34205  signsw0glem  34531  bnj1189  34986  fmlafvel  35353  gonan0  35360  satffun  35377  mvtval  35468  mexval  35470  mexval2  35471  mdvval  35472  mrsubfval  35476  mrsubrn  35481  msubfval  35492  elmsubrn  35496  msubrn  35497  mvhfval  35501  mpstval  35503  msrfval  35505  mstaval  35512  mppsval  35540  mthmval  35543  dfrdg3  35760  fvsingle  35884  unisnif  35889  funpartfv  35909  fullfunfv  35911  linedegen  36107  bj-ax6e  36632  axc11n11r  36647  bj-ax12v3ALT  36650  bj-sbsb  36801  bj-nfcsym  36863  bj-snex  36999  bj-restsnid  37051  bj-inftyexpitaudisj  37169  bj-inftyexpidisj  37174  finxpreclem4  37358  finxp00  37366  isinf2  37369  wl-nfs1t  37501  matunitlindflem1  37586  itg2addnclem  37641  ibladdnclem  37646  itgaddnclem1  37648  iblabsnc  37654  iblmulc2nc  37655  ftc1anclem8  37670  ismgmOLD  37820  tsbi1  38103  tsbi2  38104  ac6s6  38142  equid1  38863  ax12fromc15  38869  equid1ALT  38889  dvelimf-o  38893  ax12inda2ALT  38910  ax12inda2  38911  sn-axprlem3  42214  fsuppind  42560  mzpmfp  42717  itgocn  43135  mendbas  43151  mendplusgfval  43152  mendmulrfval  43154  mendsca  43156  mendvscafval  43157  arearect  43186  areaquad  43187  fpwfvss  43383  safesnsupfidom1o  43388  sn1dom  43497  or3or  43994  uneqsn  43996  addcomgi  44428  ax6e2ndeq  44532  2sb5ndVD  44882  2sb5ndALT  44904  sqwvfoura  46205  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  hspdifhsp  46593  hspmbllem2  46604  hspmbl  46606  et-ltneverrefl  46848  tz6.12-afv  47150  ndmaovcl  47180  tz6.12-afv2  47217  otiunsndisjX  47256  fvmptrab  47269  nltle2tri  47290  fzopredsuc  47300  iccpartiltu  47384  iccpartigtl  47385  iccpartlt  47386  icceuelpartlem  47397  iccpartnel  47400  elsprel  47437  sprssspr  47443  sprsymrelfvlem  47452  prprelprb  47479  prprspr2  47480  fmtnoprmfac1  47527  fmtnoprmfac2  47529  prmdvdsfmtnof1lem2  47547  prminf2  47550  lighneallem4  47572  requad1  47584  requad2  47585  evenprm2  47676  even3prm2  47681  fpprbasnn  47691  stgoldbwt  47738  upwlkbprop  48061  pgrpgt2nabl  48289  suppmptcfin  48299  linc1  48349  lindslinindsimp2lem5  48386  1aryenef  48573  2aryenef  48584  reorelicc  48638  rrxsphere  48676  fvconst0ci  48814  fvconstdomi  48815  upfval  49059  reldmprcof1  49239  reldmprcof2  49240  lmdfval  49471  cmdfval  49472  setrec2lem1  49505  setrec2mpt  49509