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  1566  ax6e  2412  ax12  2452  exdistrf  2476  equvini  2484  ax12vALT  2498  2ax6e  2500  sb1  2507  sb2  2508  sb4a  2509  dfsb1  2510  dfsb2  2522  sbcom3  2535  sbco2  2540  sbco3  2542  sb9  2548  eujustALT  2597  pm2.61ine  3038  ralcom2  3362  eueq2  3667  moeq3  3669  mo2icl  3671  sbc2or  3747  unineq  4232  csb0  4367  sbcel12  4368  sbcne12  4372  sbcel2  4375  csbidm  4390  csbun  4398  csbin  4399  csbdif  4480  ifsb  4495  ifid  4522  ifnot  4534  ifan  4535  ifor  4536  csbif  4539  elimhyp  4547  elimhyp2v  4548  elimhyp3v  4549  elimhyp4v  4550  elimdhyp  4552  keephyp2v  4554  keephyp3v  4555  rmosn  4676  rabsnif  4680  tppreqb  4764  ssunsn2  4782  n0snor2el  4787  preq12nebg  4817  opthprneg  4819  elpreqprlem  4820  dfopif  4836  csbuni  4897  disjord  5091  sbcbr  5160  unisn2  5265  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  5753  csbcnv  5865  csbres  5974  csbima12  6078  soirri  6122  csbrn  6207  dmsnopss  6218  dmsnsnsn  6224  opswap  6233  unixpid  6290  predres  6345  nsuceq0  6451  ordsssuc2  6459  iotassuni  6517  iotaex  6518  csbiota  6536  dffv3  6886  fvrn0  6918  ndmfv  6922  elfv2ex  6933  fveqres  6934  csbfv12  6935  csbfv  6937  dffv2  6985  fvco4i  6992  fvmptss  7011  fvmptex  7013  fvmptss2  7025  fvmptrabfv  7031  f0cli  7103  fvunsn  7188  fconst5  7216  csbriota  7396  riotassuni  7421  oprabidw  7455  csbov123  7468  csbov  7469  fvmptopab  7479  brfvopab  7481  elimdelov  7520  ovif12  7524  ifmpt2v  7526  ndmovcl  7610  ndmovord  7615  elovmpt3imp  7682  difsnexi  7779  ordsuc  7829  ordsucelsuc  7837  1stval  8007  2ndval  8008  1st2val  8033  2nd2val  8034  el2mpocsbcl  8101  bropopvvv  8106  bropfvvvvlem  8107  bropfvvvv  8108  suppimacnv  8199  suppssdm  8202  ressuppss  8208  suppun  8209  extmptsuppeq  8213  funsssuppss  8215  fczsupp0  8218  suppss  8219  suppss2  8225  suppssfv  8227  suppco  8231  mpoxopynvov0  8243  mpoxopoveqd  8246  pwuninelOLD  8301  smofvon2  8372  om0x  8535  mapssfset  8881  brdomg  8993  snfi  9079  sdomirr  9141  domunsn  9154  2pwuninel  9159  unfi  9194  cnvfi  9199  suppeqfsuppbi  9378  fsuppun  9386  funsnfsupp  9391  fipwuni  9425  oicl  9530  oif  9531  wemapso2  9554  card2on  9555  en2lp  9614  ttrclselem1  9733  tctr  9746  r1tr  9790  rankdmr1  9816  r1wf  9848  r1pw  9866  r1pwALT  9867  rankuni  9886  scottex  9940  scottexOLD  9941  setrec2lem1  9981  cardidm  10047  alephcard  10156  alephnbtwn  10157  cfub  10333  cardcf  10336  cflecard  10337  cfle  10338  cflim2  10348  cfidm  10360  isf32lem9  10446  itunisuc  10504  itunitc1  10505  itunitc  10506  ituniiun  10507  axcc2lem  10521  alephreg  10674  pwcfsdom  10675  cfpwsdom  10676  axunndlem1  10687  axpownd  10693  tskmcl  10933  addcompi  10986  addasspi  10987  mulcompi  10988  mulasspi  10989  distrpi  10990  addnidpi  10993  nlt1pi  10998  addcompq  11042  addcomnq  11043  mulcompq  11044  mulcomnq  11045  adderpq  11048  mulerpq  11049  addassnq  11050  mulassnq  11051  distrnq  11053  genpass  11101  addcompr  11113  mulcompr  11115  distrpr  11120  ltexprlem7  11134  addcomsr  11179  addasssr  11180  mulcomsr  11181  mulasssr  11182  distrsr  11183  indval0  12331  uzssz  12993  uzwo  13045  nn01to3  13075  xnn0xaddcl  13372  elixx3g  13496  iooid  13511  elfz2  13653  injresinjlem  13932  injresinj  13933  fleqceilz  14001  modifeq2int  14083  modfzo0difsn  14093  addmodlteq  14096  ltweuz  14111  fzofi  14124  fsuppmapnn0fiubex  14142  hashrabrsn  14523  hashrabsn01  14524  hashrabsn1  14525  elprchashprn2  14547  hashss  14560  hashsn01  14568  hash1snb  14571  hashgt12el  14574  hashgt12el2  14575  hashgt23el  14576  hashfzp1  14583  hashfundm  14594  hash2pwpr  14628  hashge2el2dif  14632  hash3tpde  14645  ffz0iswrd  14693  ccatsymb  14735  swrd00  14800  swrd0  14816  swrdwrdsymb  14820  pfx00  14832  pfx0  14833  repswswrd  14943  0csh0  14952  cshwcl  14957  cshwidxmod  14962  repswcshw  14971  cshw1  14981  s3sndisj  15129  s3iunsndisj  15130  xptrrel  15142  trclfvcotrg  15178  relexpfld  15211  reusq0  15641  modfsummods  15969  dvdsaddre2b  16486  gcdaddmlem  16705  prm23ge5  17002  pcmptcl  17078  prmgaplem5  17242  prmgaplem6  17243  cshwshash  17291  strle1  17345  strfvss  17374  strfvi  17377  setsnid  17395  ressbas  17423  ressbasssg  17424  ressbasssOLD  17427  resseqnbas  17429  ress0  17430  ressress  17434  0rest  17609  firest  17612  topnval  17614  xpsaddlem  17754  xpsvsca  17758  homffval  17873  comfffval  17881  oppchomfval  17897  oppcbas  17901  fullfunc  18092  fthfunc  18093  natfval  18133  fucbas  18147  fuchom  18148  arwval  18227  coafval  18248  xpcbas  18361  xpchomfval  18362  xpccofval  18365  oduval  18471  oduleval  18472  lubfun  18533  glbfun  18546  odujoin  18589  odumeet  18591  ipopos  18719  plusffval  18831  grpidval  18849  gsum0  18882  frmdplusg  19059  frmd0  19065  efmndbas  19076  efmndbasabf  19077  efmndplusg  19085  mgm2nsgrplem2  19127  mgm2nsgrplem3  19128  sgrp2rid2  19134  dfgrp2e  19183  grpinvfval  19198  grpinvfvalALT  19199  grpinvfvi  19202  grpsubfval  19203  grpsubfvalALT  19204  mulgfval  19288  mulgfvalALT  19289  mulgfvi  19292  cntrval  19542  oppgval  19570  oppgplusfval  19571  symgval  19594  snsymgefmndeq  19618  psgnfval  19723  odfval  19755  odfvalALT  19756  oppglsm  19865  efgval  19940  mgpval  20372  mgpplusg  20373  ringidval  20418  opprval  20577  opprmulfval  20578  dvdsrval  20600  invrfval  20628  dvrfval  20641  rrgval  20958  staffval  21107  scaffval  21164  rlmval  21475  rlmsca2  21483  2idlval  21553  nzerooringczr  21795  zrhval  21822  zlmlem  21831  zlmvsca  21836  chrval  21838  evpmss  21901  psgndiflemB  21915  ipffval  21963  thlbas  22011  thlle  22012  thloc  22014  pjfval  22021  dsmmval2  22051  asclfval  22195  psrplusg  22254  psrmulr  22259  psrvscafval  22265  mplval  22305  mplcoe3  22356  evlval  22418  psr1val  22513  vr1val  22519  ply1val  22521  ply1basfvi  22567  ply1plusgfvi  22568  psr1sca2  22577  ply1sca2  22580  ply1ascl  22586  cply1mul  22623  gsummoncoe1  22635  evl1fval  22655  evl1fval1  22658  mamufacex  22720  mavmulsolcl  22875  marrepfval  22884  marepvfval  22889  submafval  22903  mdetfval  22910  mdetfval1  22914  mdetunilem7  22942  mdetunilem8  22943  madufval  22961  minmar1fval  22970  matunitlindflem1  23003  mp2pm2mplem4  23136  toponsspwpw  23249  tgdif0  23319  indislem  23327  resstopn  23513  iocpnfordt  23542  icomnfordt  23543  hmeofval  24086  ussval  24587  nmfval  24916  nghmfval  25050  pcofval  25340  tcphval  25548  ioombl  25895  ibladdlem  26149  itgaddlem1  26152  iblabs  26158  dvbsss  26231  perfdvf  26232  mdegfval  26389  deg1fval  26407  deg1fvi  26412  uc1pval  26467  mon1pval  26469  2irrexpq  27068  lgsqrmodndvds  27689  gausslemma2dlem1a  27701  2lgs  27743  2sqreultblem  27784  2sqreunnltblem  27787  newval  28230  leftval  28244  rightval  28245  lltr  28257  oldssmade  28262  oldss  28265  lrold  28292  ttglem  29462  axcontlem12  29562  vtxval  29587  iedgval  29588  edgval  29636  usgr1v  29846  nbuhgr  29933  nbumgr  29937  uhgrnbgr0nb  29944  nbgr1vtx  29948  nbgrnself2  29950  nbusgrvtxm1  29969  sizusglecusg  30053  g0wlk0  30240  wlkreslem  30257  lfgrwlkprop  30279  wwlks  30433  wwlksn  30435  wspthsn  30446  iswwlksnon  30451  iswspthsnon  30454  0enwwlksnge1  30462  wwlksnfi  30504  clwwlk  30583  umgrclwwlkge2  30591  clwlkclwwlklem2a4  30597  clwwlkn  30626  clwwlknonmpo  30689  clwwlknon  30690  clwwlk0on0  30692  clwwlknon1le1  30701  1conngr  30804  eupth2lem3lem7  30844  frgr1v  30881  nfrgr2v  30882  1to2vfriswmgr  30889  2wspmdisj  30947  frgrreggt1  31003  frgrreg  31004  frgrregord013  31005  frgrogt3nreg  31007  friendship  31009  avril1  31073  vafval  31214  bafval  31215  smfval  31216  vsfval  31244  bcsiALT  31790  of0r  33324  fracval  33916  fracbas  33917  resvsca  33943  resvlem  33944  cntnevol  34911  signsw0glem  35232  bnj1189  35689  rankscottu  35815  noinfepregs  35869  kardval  35888  kard0b  35895  kardcard2b  35901  rankkardu  35907  j0ltaleph  35959  k1on  35966  k2on  35967  k39o  35968  fmlafvel  36268  gonan0  36275  satffun  36292  mvtval  36383  mexval  36385  mexval2  36386  mdvval  36387  mrsubfval  36391  mrsubrn  36396  msubfval  36407  elmsubrn  36411  msubrn  36412  mvhfval  36416  mpstval  36418  msrfval  36420  mstaval  36427  mppsval  36455  mthmval  36458  antnestlaw2  36575  dfrdg3  36682  fvsingle  36806  unisnif  36811  funpartfv  36833  fullfunfv  36835  linedegen  37032  axtcond  37390  csbttc  37421  mh-setindnd  37449  bj-ax6e  37691  axc11n11r  37709  bj-ax12v3ALT  37712  bj-sbsb  37873  bj-nfcsym  37935  bj-snex  38072  bj-restsnid  38144  bj-inftyexpitaudisj  38263  bj-inftyexpidisj  38268  finxpreclem4  38454  finxp00  38462  isinf2  38465  wl-nfs1t  38606  itg2addnclem  38726  ibladdnclem  38731  itgaddnclem1  38733  iblabsnc  38739  iblmulc2nc  38740  ftc1anclem8  38755  ismgmOLD  38921  tsbi1  39202  tsbi2  39203  ac6s6  39241  equid1  40093  ax12fromc15  40099  equid1ALT  40119  dvelimf-o  40123  ax12inda2ALT  40140  ax12inda2  40141  sn-axprlem3  43409  fsuppind  43755  mzpmfp  43895  itgocn  44303  mendbas  44319  mendplusgfval  44320  mendmulrfval  44322  mendsca  44324  mendvscafval  44325  arearect  44354  areaquad  44355  fpwfvss  44550  safesnsupfidom1o  44555  sn1dom  44664  or3or  45160  uneqsn  45162  addcomgi  45574  ax6e2ndeq  45678  2sb5ndVD  46028  2sb5ndALT  46050  sqwvfoura  47374  sqwvfourb  47375  fourierswlem  47376  fouriersw  47377  hspdifhsp  47762  hspmbllem2  47773  hspmbl  47775  et-ltneverrefl  48017  aiotaexim  48304  tz6.12-afv  48379  ndmaovcl  48409  tz6.12-afv2  48446  otiunsndisjX  48485  fvmptrab  48498  nltle2tri  48519  fzopredsuc  48530  iccpartiltu  48640  iccpartigtl  48641  iccpartlt  48642  icceuelpartlem  48653  iccpartnel  48656  elsprel  48693  sprssspr  48699  sprsymrelfvlem  48708  prprelprb  48735  prprspr2  48736  fmtnoprmfac1  48786  fmtnoprmfac2  48788  prmdvdsfmtnof1lem2  48806  prminf2  48809  lighneallem4  48831  requad1  48856  requad2  48857  evenprm2  48948  even3prm2  48953  fpprbasnn  48963  stgoldbwt  49010  pgnbgreunbgrlem2lem1  49348  pgnbgreunbgrlem2lem2  49349  pgnbgreunbgrlem2lem3  49350  upwlkbprop  49372  pgrpgt2nabl  49614  suppmptcfin  49624  linc1  49673  lindslinindsimp2lem5  49710  1aryenef  49893  2aryenef  49904  reorelicc  49958  rrxsphere  49996  fvconst0ci  50141  fvconstdomi  50142  upfval  50428  reldmprcof1  50652  reldmprcof2  50653  lmdfval  50968  cmdfval  50969  setrec2mpt  51001