Theorem pm2.61i 184

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 159	. 2 ⊢ (¬ 𝜓 → 𝜓)
4	3	pm2.18i 130	1 ⊢ 𝜓

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.61ii  185  pm2.61nii  186  pm2.61iii  187  pm2.65iOLD  197  pm5.21nii  381  pm5.18  384  biass  388  pm2.61ian  824  ecase3  1048  4cases  1056  pm4.42  1069  ifpid  1093  elimh  1099  3ecase  1505  norass  1567  ax6e  2413  ax12  2453  exdistrf  2477  equvini  2485  ax12vALT  2499  2ax6e  2501  sb1  2508  sb2  2509  sb4a  2510  dfsb1  2511  dfsb2  2523  sbcom3  2536  sbco2  2541  sbco3  2543  sb9  2549  eujustALT  2598  pm2.61ine  3039  ralcom2  3363  eueq2  3668  moeq3  3670  mo2icl  3672  sbc2or  3748  unineq  4234  csb0  4368  sbcel12  4369  sbcne12  4373  sbcel2  4376  csbidm  4391  csbun  4399  csbin  4400  csbdif  4481  ifsb  4496  ifid  4523  ifnot  4535  ifan  4536  ifor  4537  csbif  4540  elimhyp  4548  elimhyp2v  4549  elimhyp3v  4550  elimhyp4v  4551  elimdhyp  4553  keephyp2v  4555  keephyp3v  4556  rmosn  4680  rabsnif  4684  tppreqb  4768  ssunsn2  4788  n0snor2el  4793  preq12nebg  4823  opthprneg  4825  elpreqprlem  4826  dfopif  4830  csbuni  4898  disjord  5092  sbcbr  5160  unisn2  5266  intabs  5310  class2set  5316  dtruALT2  5332  snexALT  5345  dtruALT  5350  axprlem3  5387  axprglem  5394  axprg  5395  snexOLD  5400  exneq  5404  copsexgwOLD  5461  copsexg  5462  snopeqop  5478  csbopab  5530  dfid3  5549  csbxp  5752  csbcnv  5864  csbres  5973  csbima12  6076  soirri  6120  csbrn  6204  dmsnopss  6215  dmsnsnsn  6221  opswap  6230  unixpid  6287  predres  6342  nsuceq0  6448  ordsssuc2  6456  iotassuni  6513  iotaex  6514  csbiota  6531  dffv3  6881  fvrn0  6913  ndmfv  6917  elfv2ex  6928  fveqres  6929  csbfv12  6930  csbfv  6932  dffv2  6980  fvco4i  6987  fvmptss  7006  fvmptex  7008  fvmptss2  7020  fvmptrabfv  7026  f0cli  7098  fvunsn  7184  fconst5  7212  csbriota  7392  riotassuni  7417  oprabidw  7451  csbov123  7464  csbov  7465  fvmptopab  7475  brfvopab  7477  elimdelov  7516  ovif12  7520  ifmpt2v  7522  ndmovcl  7606  ndmovord  7611  elovmpt3imp  7678  difsnexi  7775  ordsuc  7825  ordsucelsuc  7833  1stval  8003  2ndval  8004  1st2val  8029  2nd2val  8030  el2mpocsbcl  8096  bropopvvv  8101  bropfvvvvlem  8102  bropfvvvv  8103  suppimacnv  8191  suppssdm  8194  ressuppss  8200  suppun  8201  extmptsuppeq  8205  funsssuppss  8207  fczsupp0  8210  suppss  8211  suppss2  8217  suppssfv  8219  suppco  8223  mpoxopynvov0  8235  mpoxopoveqd  8238  pwuninelOLD  8293  smofvon2  8364  om0x  8527  mapssfset  8873  brdomg  8985  snfi  9071  sdomirr  9133  domunsn  9146  2pwuninel  9151  unfi  9186  cnvfi  9191  suppeqfsuppbi  9371  fsuppun  9379  funsnfsupp  9384  fipwuni  9418  oicl  9523  oif  9524  wemapso2  9547  card2on  9548  en2lp  9607  ttrclselem1  9726  tctr  9739  r1tr  9783  rankdmr1  9809  r1wf  9841  r1pw  9859  r1pwALT  9860  rankuni  9879  scottex  9933  scottexOLD  9934  setrec2lem1  9974  cardidm  10040  alephcard  10149  alephnbtwn  10150  cfub  10326  cardcf  10329  cflecard  10330  cfle  10331  cflim2  10341  cfidm  10353  isf32lem9  10439  itunisuc  10497  itunitc1  10498  itunitc  10499  ituniiun  10500  axcc2lem  10514  alephreg  10667  pwcfsdom  10668  cfpwsdom  10669  axunndlem1  10680  axpownd  10686  tskmcl  10926  addcompi  10979  addasspi  10980  mulcompi  10981  mulasspi  10982  distrpi  10983  addnidpi  10986  nlt1pi  10991  addcompq  11035  addcomnq  11036  mulcompq  11037  mulcomnq  11038  adderpq  11041  mulerpq  11042  addassnq  11043  mulassnq  11044  distrnq  11046  genpass  11094  addcompr  11106  mulcompr  11108  distrpr  11113  ltexprlem7  11127  addcomsr  11172  addasssr  11173  mulcomsr  11174  mulasssr  11175  distrsr  11176  indval0  12324  uzssz  12986  uzwo  13038  nn01to3  13068  xnn0xaddcl  13365  elixx3g  13489  iooid  13504  elfz2  13646  injresinjlem  13925  injresinj  13926  fleqceilz  13994  modifeq2int  14076  modfzo0difsn  14086  addmodlteq  14089  ltweuz  14104  fzofi  14117  fsuppmapnn0fiubex  14135  hashrabrsn  14516  hashrabsn01  14517  hashrabsn1  14518  elprchashprn2  14540  hashss  14553  hashsn01  14561  hash1snb  14564  hashgt12el  14567  hashgt12el2  14568  hashgt23el  14569  hashfzp1  14576  hashfundm  14587  hash2pwpr  14621  hashge2el2dif  14625  hash3tpde  14638  ffz0iswrd  14686  ccatsymb  14728  swrd00  14792  swrd0  14808  swrdwrdsymb  14812  pfx00  14824  pfx0  14825  repswswrd  14935  0csh0  14944  cshwcl  14949  cshwidxmod  14954  repswcshw  14963  cshw1  14973  s3sndisj  15120  s3iunsndisj  15121  xptrrel  15133  trclfvcotrg  15169  relexpfld  15202  reusq0  15632  modfsummods  15960  dvdsaddre2b  16477  gcdaddmlem  16696  prm23ge5  16993  pcmptcl  17069  prmgaplem5  17233  prmgaplem6  17234  cshwshash  17282  strle1  17336  strfvss  17365  strfvi  17368  setsnid  17386  ressbas  17414  ressbasssg  17415  ressbasssOLD  17418  resseqnbas  17420  ress0  17421  ressress  17425  0rest  17600  firest  17603  topnval  17605  xpsaddlem  17745  xpsvsca  17749  homffval  17864  comfffval  17872  oppchomfval  17888  oppcbas  17892  fullfunc  18083  fthfunc  18084  natfval  18124  fucbas  18138  fuchom  18139  arwval  18218  coafval  18239  xpcbas  18352  xpchomfval  18353  xpccofval  18356  oduval  18462  oduleval  18463  lubfun  18524  glbfun  18537  odujoin  18580  odumeet  18582  ipopos  18710  plusffval  18822  grpidval  18840  gsum0  18873  frmdplusg  19050  frmd0  19056  efmndbas  19067  efmndbasabf  19068  efmndplusg  19076  mgm2nsgrplem2  19118  mgm2nsgrplem3  19119  sgrp2rid2  19125  dfgrp2e  19174  grpinvfval  19189  grpinvfvalALT  19190  grpinvfvi  19193  grpsubfval  19194  grpsubfvalALT  19195  mulgfval  19279  mulgfvalALT  19280  mulgfvi  19283  cntrval  19533  oppgval  19561  oppgplusfval  19562  symgval  19585  snsymgefmndeq  19609  psgnfval  19714  odfval  19746  odfvalALT  19747  oppglsm  19856  efgval  19931  mgpval  20363  mgpplusg  20364  ringidval  20409  opprval  20568  opprmulfval  20569  dvdsrval  20591  invrfval  20619  dvrfval  20632  rrgval  20949  staffval  21098  scaffval  21155  rlmval  21466  rlmsca2  21474  2idlval  21544  nzerooringczr  21786  zrhval  21813  zlmlem  21822  zlmvsca  21827  chrval  21829  evpmss  21892  psgndiflemB  21906  ipffval  21954  thlbas  22002  thlle  22003  thloc  22005  pjfval  22012  dsmmval2  22042  asclfval  22186  psrplusg  22245  psrmulr  22250  psrvscafval  22256  mplval  22296  mplcoe3  22347  evlval  22409  psr1val  22504  vr1val  22510  ply1val  22512  ply1basfvi  22558  ply1plusgfvi  22559  psr1sca2  22568  ply1sca2  22571  ply1ascl  22577  cply1mul  22614  gsummoncoe1  22626  evl1fval  22646  evl1fval1  22649  mamufacex  22711  mavmulsolcl  22866  marrepfval  22875  marepvfval  22880  submafval  22894  mdetfval  22901  mdetfval1  22905  mdetunilem7  22933  mdetunilem8  22934  madufval  22952  minmar1fval  22961  matunitlindflem1  22994  mp2pm2mplem4  23127  toponsspwpw  23240  tgdif0  23310  indislem  23318  resstopn  23504  iocpnfordt  23533  icomnfordt  23534  hmeofval  24077  ussval  24578  nmfval  24907  nghmfval  25041  pcofval  25331  tcphval  25539  ioombl  25886  ibladdlem  26140  itgaddlem1  26143  iblabs  26149  dvbsss  26222  perfdvf  26223  mdegfval  26380  deg1fval  26398  deg1fvi  26403  uc1pval  26458  mon1pval  26460  2irrexpq  27059  lgsqrmodndvds  27680  gausslemma2dlem1a  27692  2lgs  27734  2sqreultblem  27775  2sqreunnltblem  27778  newval  28221  leftval  28235  rightval  28236  lltr  28248  oldssmade  28253  oldss  28256  lrold  28283  ttglem  29453  axcontlem12  29553  vtxval  29578  iedgval  29579  edgval  29627  usgr1v  29837  nbuhgr  29924  nbumgr  29928  uhgrnbgr0nb  29935  nbgr1vtx  29939  nbgrnself2  29941  nbusgrvtxm1  29960  sizusglecusg  30044  g0wlk0  30231  wlkreslem  30248  lfgrwlkprop  30270  wwlks  30424  wwlksn  30426  wspthsn  30437  iswwlksnon  30442  iswspthsnon  30445  0enwwlksnge1  30453  wwlksnfi  30495  clwwlk  30574  umgrclwwlkge2  30582  clwlkclwwlklem2a4  30588  clwwlkn  30617  clwwlknonmpo  30680  clwwlknon  30681  clwwlk0on0  30683  clwwlknon1le1  30692  1conngr  30795  eupth2lem3lem7  30835  frgr1v  30872  nfrgr2v  30873  1to2vfriswmgr  30880  2wspmdisj  30938  frgrreggt1  30994  frgrreg  30995  frgrregord013  30996  frgrogt3nreg  30998  friendship  31000  avril1  31064  vafval  31205  bafval  31206  smfval  31207  vsfval  31235  bcsiALT  31781  of0r  33273  fracval  33866  fracbas  33867  resvsca  33893  resvlem  33894  cntnevol  34861  signsw0glem  35182  bnj1189  35639  rankscottu  35753  noinfepregs  35801  kardval  35820  kard0b  35827  kardcard2b  35833  rankkardu  35839  fmlafvel  36150  gonan0  36157  satffun  36174  mvtval  36265  mexval  36267  mexval2  36268  mdvval  36269  mrsubfval  36273  mrsubrn  36278  msubfval  36289  elmsubrn  36293  msubrn  36294  mvhfval  36298  mpstval  36300  msrfval  36302  mstaval  36309  mppsval  36337  mthmval  36340  antnestlaw2  36457  dfrdg3  36558  fvsingle  36682  unisnif  36687  funpartfv  36709  fullfunfv  36711  linedegen  36908  axtcond  37266  csbttc  37297  mh-setindnd  37325  bj-ax6e  37567  axc11n11r  37585  bj-ax12v3ALT  37588  bj-sbsb  37749  bj-nfcsym  37811  bj-snex  37948  bj-restsnid  38008  bj-inftyexpitaudisj  38126  bj-inftyexpidisj  38131  finxpreclem4  38317  finxp00  38325  isinf2  38328  wl-nfs1t  38469  itg2addnclem  38589  ibladdnclem  38594  itgaddnclem1  38596  iblabsnc  38602  iblmulc2nc  38603  ftc1anclem8  38618  ismgmOLD  38784  tsbi1  39065  tsbi2  39066  ac6s6  39104  equid1  39956  ax12fromc15  39962  equid1ALT  39982  dvelimf-o  39986  ax12inda2ALT  40003  ax12inda2  40004  sn-axprlem3  43272  fsuppind  43618  mzpmfp  43757  itgocn  44165  mendbas  44181  mendplusgfval  44182  mendmulrfval  44184  mendsca  44186  mendvscafval  44187  arearect  44216  areaquad  44217  fpwfvss  44412  safesnsupfidom1o  44417  sn1dom  44526  or3or  45022  uneqsn  45024  addcomgi  45437  ax6e2ndeq  45541  2sb5ndVD  45891  2sb5ndALT  45913  sqwvfoura  47237  sqwvfourb  47238  fourierswlem  47239  fouriersw  47240  hspdifhsp  47625  hspmbllem2  47636  hspmbl  47638  et-ltneverrefl  47880  tz6.12-afv  48242  ndmaovcl  48272  tz6.12-afv2  48309  otiunsndisjX  48348  fvmptrab  48361  nltle2tri  48382  fzopredsuc  48393  iccpartiltu  48503  iccpartigtl  48504  iccpartlt  48505  icceuelpartlem  48516  iccpartnel  48519  elsprel  48556  sprssspr  48562  sprsymrelfvlem  48571  prprelprb  48598  prprspr2  48599  fmtnoprmfac1  48649  fmtnoprmfac2  48651  prmdvdsfmtnof1lem2  48669  prminf2  48672  lighneallem4  48694  requad1  48719  requad2  48720  evenprm2  48811  even3prm2  48816  fpprbasnn  48826  stgoldbwt  48873  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  pgnbgreunbgrlem2lem3  49213  upwlkbprop  49235  pgrpgt2nabl  49477  suppmptcfin  49487  linc1  49536  lindslinindsimp2lem5  49573  1aryenef  49756  2aryenef  49767  reorelicc  49821  rrxsphere  49859  fvconst0ci  49998  fvconstdomi  49999  upfval  50283  reldmprcof1  50488  reldmprcof2  50489  lmdfval  50756  cmdfval  50757  setrec2mpt  50789