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  3348  eueq2  3678  moeq3  3680  mo2icl  3682  sbc2or  3759  unineq  4247  csb0  4369  sbcel12  4370  sbcne12  4374  sbcel2  4377  csbidm  4392  csbun  4400  csbin  4401  csbdif  4483  ifsb  4498  ifid  4525  ifnot  4537  ifan  4538  ifor  4539  csbif  4542  elimhyp  4550  elimhyp2v  4551  elimhyp3v  4552  elimhyp4v  4553  elimdhyp  4555  keephyp2v  4557  keephyp3v  4558  rmosn  4679  rabsnif  4683  tppreqb  4765  ssunsn2  4787  n0snor2el  4793  preq12nebg  4823  opthprneg  4825  elpreqprlem  4826  dfopif  4830  csbuni  4896  disjord  5091  sbcbr  5157  unisn2  5262  intabs  5299  class2set  5305  dtruALT2  5320  snexALT  5333  dtruALT  5338  axprlem3  5375  axprlem3OLD  5378  snex  5386  exneq  5390  dtruOLD  5396  copsexgw  5445  copsexg  5446  snopeqop  5461  csbopab  5510  dfid3  5529  csbxp  5730  csbres  5942  csbima12  6039  soirri  6087  csbrn  6164  dmsnopss  6175  dmsnsnsn  6181  opswap  6190  unixpid  6245  predres  6300  nsuceq0  6405  ordsssuc2  6413  iotassuni  6471  iotaex  6472  iotassuniOLD  6478  iotaexOLD  6479  csbiota  6492  dffv3  6836  fvrn0  6870  ndmfv  6875  elfv2ex  6886  fveqres  6887  csbfv12  6888  csbfv  6890  dffv2  6938  fvco4i  6944  fvmptss  6962  fvmptex  6964  fvmptss2  6976  fvmptrabfv  6982  f0cli  7052  fvunsn  7135  fconst5  7162  csbriota  7341  riotassuni  7366  oprabidw  7400  csbov123  7413  csbov  7414  fvmptopab  7424  brfvopab  7426  elimdelov  7465  ovif12  7469  ifmpt2v  7471  ndmovcl  7554  ndmovord  7559  elovmpt3imp  7626  difsnexi  7717  ordsuc  7768  ordsucOLD  7769  ordsucelsuc  7777  1stval  7949  2ndval  7950  1st2val  7975  2nd2val  7976  el2mpocsbcl  8041  bropopvvv  8046  bropfvvvvlem  8047  bropfvvvv  8048  suppimacnv  8130  suppssdm  8133  ressuppss  8139  suppun  8140  extmptsuppeq  8144  funsssuppss  8146  fczsupp0  8149  suppss  8150  suppss2  8156  suppssfv  8158  suppco  8162  mpoxopynvov0  8174  mpoxopoveqd  8177  pwuninel  8231  smofvon2  8302  om0x  8460  mapssfset  8801  brdomg  8907  snfi  8991  snfiOLD  8992  sdomirr  9055  domunsn  9068  2pwuninel  9073  unfi  9112  cnvfi  9117  suppeqfsuppbi  9306  fsuppun  9314  funsnfsupp  9319  fipwuni  9353  oicl  9458  oif  9459  wemapso2  9482  card2on  9483  en2lp  9535  ttrclselem1  9654  tctr  9669  r1tr  9705  rankdmr1  9730  r1pw  9774  r1pwALT  9775  rankuni  9792  scottex  9814  cardidm  9888  alephcard  9999  alephnbtwn  10000  cfub  10178  cardcf  10181  cflecard  10182  cfle  10183  cflim2  10192  cfidm  10204  isf32lem9  10290  itunisuc  10348  itunitc1  10349  itunitc  10350  ituniiun  10351  axcc2lem  10365  alephreg  10511  pwcfsdom  10512  cfpwsdom  10513  axunndlem1  10524  axpownd  10530  tskmcl  10770  addcompi  10823  addasspi  10824  mulcompi  10825  mulasspi  10826  distrpi  10827  addnidpi  10830  nlt1pi  10835  addcompq  10879  addcomnq  10880  mulcompq  10881  mulcomnq  10882  adderpq  10885  mulerpq  10886  addassnq  10887  mulassnq  10888  distrnq  10890  genpass  10938  addcompr  10950  mulcompr  10952  distrpr  10957  ltexprlem7  10971  addcomsr  11016  addasssr  11017  mulcomsr  11018  mulasssr  11019  distrsr  11020  uzssz  12790  uzwo  12846  nn01to3  12876  xnn0xaddcl  13171  elixx3g  13295  iooid  13310  elfz2  13451  injresinjlem  13724  injresinj  13725  fleqceilz  13792  modifeq2int  13874  modfzo0difsn  13884  addmodlteq  13887  ltweuz  13902  fzofi  13915  fsuppmapnn0fiubex  13933  hashrabrsn  14313  hashrabsn01  14314  hashrabsn1  14315  elprchashprn2  14337  hashss  14350  hashsn01  14357  hash1snb  14360  hashgt12el  14363  hashgt12el2  14364  hashgt23el  14365  hashfzp1  14372  hashfundm  14383  hash2pwpr  14417  hashge2el2dif  14421  hash3tpde  14434  ffz0iswrd  14482  ccatsymb  14523  swrd00  14585  swrd0  14599  swrdwrdsymb  14603  pfx00  14615  pfx0  14616  repswswrd  14725  0csh0  14734  cshwcl  14739  cshwidxmod  14744  repswcshw  14753  cshw1  14763  s3sndisj  14909  s3iunsndisj  14910  xptrrel  14922  trclfvcotrg  14958  relexpfld  14991  reusq0  15407  modfsummods  15735  dvdsaddre2b  16253  gcdaddmlem  16470  prm23ge5  16762  pcmptcl  16838  prmgaplem5  17002  prmgaplem6  17003  cshwshash  17051  strle1  17104  strfvss  17133  strfvi  17136  setsnid  17154  ressbas  17182  ressbasssg  17183  ressbasssOLD  17186  resseqnbas  17188  ress0  17189  ressress  17193  0rest  17368  firest  17371  topnval  17373  xpsaddlem  17512  xpsvsca  17516  homffval  17627  comfffval  17635  oppchomfval  17651  oppcbas  17655  fullfunc  17846  fthfunc  17847  natfval  17887  fucbas  17901  fuchom  17902  arwval  17981  coafval  18002  xpcbas  18115  xpchomfval  18116  xpccofval  18119  oduval  18225  oduleval  18226  lubfun  18287  glbfun  18300  odujoin  18343  odumeet  18345  ipopos  18471  plusffval  18549  grpidval  18564  gsum0  18587  frmdplusg  18757  frmd0  18763  efmndbas  18774  efmndbasabf  18775  efmndplusg  18783  mgm2nsgrplem2  18822  mgm2nsgrplem3  18823  sgrp2rid2  18829  dfgrp2e  18871  grpinvfval  18886  grpinvfvalALT  18887  grpinvfvi  18890  grpsubfval  18891  grpsubfvalALT  18892  mulgfval  18977  mulgfvalALT  18978  mulgfvi  18981  cntrval  19227  oppgval  19255  oppgplusfval  19256  symgval  19277  snsymgefmndeq  19301  psgnfval  19406  odfval  19438  odfvalALT  19439  oppglsm  19548  efgval  19623  mgpval  20028  mgpplusg  20029  ringidval  20068  opprval  20223  opprmulfval  20224  dvdsrval  20246  invrfval  20274  dvrfval  20287  rrgval  20582  staffval  20726  scaffval  20762  rlmval  21074  rlmsca2  21082  2idlval  21137  nzerooringczr  21366  zrhval  21393  zlmlem  21402  zlmvsca  21407  chrval  21409  evpmss  21471  psgndiflemB  21485  ipffval  21533  thlbas  21581  thlle  21582  thloc  21584  pjfval  21591  dsmmval2  21621  asclfval  21764  psrplusg  21821  psrmulr  21827  psrvscafval  21833  mplval  21874  mplcoe3  21921  evlval  21978  psr1val  22046  vr1val  22052  ply1val  22054  ply1basfvi  22101  ply1plusgfvi  22102  psr1sca2  22111  ply1sca2  22114  ply1ascl  22120  cply1mul  22159  gsummoncoe1  22171  evl1fval  22191  evl1fval1  22194  mamufacex  22259  mavmulsolcl  22414  marrepfval  22423  marepvfval  22428  submafval  22442  mdetfval  22449  mdetfval1  22453  mdetunilem7  22481  mdetunilem8  22482  madufval  22500  minmar1fval  22509  mp2pm2mplem4  22672  toponsspwpw  22785  tgdif0  22855  indislem  22863  resstopn  23049  iocpnfordt  23078  icomnfordt  23079  hmeofval  23621  ussval  24123  nmfval  24452  nghmfval  24586  pcofval  24886  tcphval  25094  ioombl  25442  ibladdlem  25697  itgaddlem1  25700  iblabs  25706  dvbsss  25779  perfdvf  25780  mdegfval  25943  deg1fval  25961  deg1fvi  25966  uc1pval  26021  mon1pval  26023  2irrexpq  26616  lgsqrmodndvds  27240  gausslemma2dlem1a  27252  2lgs  27294  2sqreultblem  27335  2sqreunnltblem  27338  newval  27739  leftval  27747  rightval  27748  lltropt  27760  oldssmade  27765  lrold  27784  ttglem  28779  axcontlem12  28878  vtxval  28903  iedgval  28904  edgval  28952  usgr1v  29159  nbuhgr  29246  nbumgr  29250  uhgrnbgr0nb  29257  nbgr1vtx  29261  nbgrnself2  29263  nbusgrvtxm1  29282  sizusglecusg  29367  g0wlk0  29554  wlkreslem  29571  lfgrwlkprop  29589  wwlks  29738  wwlksn  29740  wspthsn  29751  iswwlksnon  29756  iswspthsnon  29759  0enwwlksnge1  29767  wwlksnfi  29809  clwwlk  29885  umgrclwwlkge2  29893  clwlkclwwlklem2a4  29899  clwwlkn  29928  clwwlknonmpo  29991  clwwlknon  29992  clwwlk0on0  29994  clwwlknon1le1  30003  1conngr  30096  eupth2lem3lem7  30136  frgr1v  30173  nfrgr2v  30174  1to2vfriswmgr  30181  2wspmdisj  30239  frgrreggt1  30295  frgrreg  30296  frgrregord013  30297  frgrogt3nreg  30299  friendship  30301  avril1  30365  vafval  30505  bafval  30506  smfval  30507  vsfval  30535  bcsiALT  31081  of0r  32575  fracval  33227  fracbas  33228  resvsca  33277  resvlem  33278  cntnevol  34191  signsw0glem  34517  bnj1189  34972  fmlafvel  35345  gonan0  35352  satffun  35369  mvtval  35460  mexval  35462  mexval2  35463  mdvval  35464  mrsubfval  35468  mrsubrn  35473  msubfval  35484  elmsubrn  35488  msubrn  35489  mvhfval  35493  mpstval  35495  msrfval  35497  mstaval  35504  mppsval  35532  mthmval  35535  antnestlaw2  35652  dfrdg3  35757  fvsingle  35881  unisnif  35886  funpartfv  35906  fullfunfv  35908  linedegen  36104  bj-ax6e  36629  axc11n11r  36644  bj-ax12v3ALT  36647  bj-sbsb  36798  bj-nfcsym  36860  bj-snex  36996  bj-restsnid  37048  bj-inftyexpitaudisj  37166  bj-inftyexpidisj  37171  finxpreclem4  37355  finxp00  37363  isinf2  37366  wl-nfs1t  37498  matunitlindflem1  37583  itg2addnclem  37638  ibladdnclem  37643  itgaddnclem1  37645  iblabsnc  37651  iblmulc2nc  37652  ftc1anclem8  37667  ismgmOLD  37817  tsbi1  38100  tsbi2  38101  ac6s6  38139  equid1  38865  ax12fromc15  38871  equid1ALT  38891  dvelimf-o  38895  ax12inda2ALT  38912  ax12inda2  38913  sn-axprlem3  42178  fsuppind  42551  mzpmfp  42708  itgocn  43126  mendbas  43142  mendplusgfval  43143  mendmulrfval  43145  mendsca  43147  mendvscafval  43148  arearect  43177  areaquad  43178  fpwfvss  43374  safesnsupfidom1o  43379  sn1dom  43488  or3or  43985  uneqsn  43987  addcomgi  44418  ax6e2ndeq  44522  2sb5ndVD  44872  2sb5ndALT  44894  sqwvfoura  46199  sqwvfourb  46200  fourierswlem  46201  fouriersw  46202  hspdifhsp  46587  hspmbllem2  46598  hspmbl  46600  et-ltneverrefl  46842  tz6.12-afv  47147  ndmaovcl  47177  tz6.12-afv2  47214  otiunsndisjX  47253  fvmptrab  47266  nltle2tri  47287  fzopredsuc  47297  iccpartiltu  47396  iccpartigtl  47397  iccpartlt  47398  icceuelpartlem  47409  iccpartnel  47412  elsprel  47449  sprssspr  47455  sprsymrelfvlem  47464  prprelprb  47491  prprspr2  47492  fmtnoprmfac1  47539  fmtnoprmfac2  47541  prmdvdsfmtnof1lem2  47559  prminf2  47562  lighneallem4  47584  requad1  47596  requad2  47597  evenprm2  47688  even3prm2  47693  fpprbasnn  47703  stgoldbwt  47750  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  upwlkbprop  48099  pgrpgt2nabl  48327  suppmptcfin  48337  linc1  48387  lindslinindsimp2lem5  48424  1aryenef  48607  2aryenef  48618  reorelicc  48672  rrxsphere  48710  fvconst0ci  48852  fvconstdomi  48853  upfval  49138  reldmprcof1  49343  reldmprcof2  49344  lmdfval  49611  cmdfval  49612  setrec2lem1  49655  setrec2mpt  49659