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 161	. 2 ⊢ (¬ 𝜓 → 𝜓)
4	3	pm2.18i 131	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  185  pm2.61nii  186  pm2.61iii  187  pm2.65i  196  pm5.21nii  382  pm5.18  385  biass  388  pm2.61ian  810  ecase3  1027  4cases  1035  pm4.42  1048  ifpid  1070  elimh  1076  elimhOLD  1077  3ecase  1470  norass  1533  ax6e  2401  ax12  2445  exdistrf  2469  equvini  2477  equviniOLD  2478  ax12vALT  2492  2ax6e  2494  2ax6eOLD  2495  sb1  2503  sb2  2504  sb1OLD  2507  sb4a  2509  dfsb1  2510  dfsb2  2532  sbequiOLD  2534  sbi1OLD  2542  sbcom3  2548  sbco2  2553  sbco3  2555  sb9  2561  nfsbOLD  2566  sbalOLD  2575  dfsb2ALT  2591  sbequiALT  2596  sbi1ALT  2606  sbco2ALT  2615  eujustALT  2657  pm2.61ine  3100  ralcom2  3363  eueq2  3701  moeq3  3703  mo2icl  3705  sbc2or  3781  unineq  4254  csb0  4359  sbcel12  4360  sbcne12  4364  sbcel2  4367  csbidm  4382  csbun  4390  csbin  4391  ralidm  4455  ifsb  4480  ifid  4506  ifnot  4517  ifan  4518  ifor  4519  csbif  4522  elimhyp  4530  elimhyp2v  4531  elimhyp3v  4532  elimhyp4v  4533  elimdhyp  4535  keephyp2v  4537  keephyp3v  4538  rmosn  4655  rabsnif  4659  tppreqb  4738  ssunsn2  4760  n0snor2el  4764  preq12nebg  4793  opthprneg  4795  elpreqprlem  4796  dfopif  4800  csbuni  4867  disjord  5054  sbcbr  5121  unisn2  5216  intabs  5245  class2set  5254  dtru  5271  snexALT  5284  dtruALT  5289  axprlem3  5326  snex  5332  dtruALT2  5336  copsexgw  5381  copsexg  5382  snopeqop  5396  csbopab  5442  0nelopab  5452  dfid3  5462  csbxp  5650  csbres  5856  csbima12  5947  soirri  5986  csbrn  6060  dmsnopss  6071  dmsnsnsn  6077  opswap  6086  unixpid  6135  nsuceq0  6271  ordsssuc2  6279  iotassuni  6334  iotaex  6335  csbiota  6348  dffv3  6666  fvrn0  6698  ndmfv  6700  elfv2ex  6711  fveqres  6712  csbfv12  6713  csbfv  6715  dffv2  6756  fvco4i  6762  fvmptss  6780  fvmptex  6782  fvmptss2  6793  fvmptrabfv  6799  f0cli  6864  fvunsn  6941  fconst5  6968  csbriota  7129  riotassuni  7154  oprabidw  7187  csbov123  7198  csbov  7199  fvmptopab  7209  brfvopab  7211  elimdelov  7250  ovif12  7253  ndmovcl  7333  ndmovord  7338  elovmpt3imp  7402  difsnexi  7483  ordsuc  7529  ordsucelsuc  7537  1stval  7691  2ndval  7692  1st2val  7717  2nd2val  7718  el2mpocsbcl  7780  bropopvvv  7785  bropfvvvvlem  7786  bropfvvvv  7787  suppimacnv  7841  suppssdm  7843  ressuppss  7849  suppun  7850  extmptsuppeq  7854  funsssuppss  7856  fczsupp0  7859  suppss  7860  suppssov1  7862  suppss2  7864  suppssfv  7866  suppco  7870  supp0cosupp0OLD  7873  imacosuppOLD  7875  mpoxopynvov0  7884  mpoxopoveqd  7887  pwuninel  7941  smofvon2  7993  om0x  8144  brdomg  8519  snfi  8594  sdomirr  8654  domunsn  8667  2pwuninel  8672  snnen2o  8707  suppeqfsuppbi  8847  fsuppun  8852  funsnfsupp  8857  fipwuni  8890  oicl  8993  oif  8994  wemapso2  9017  card2on  9018  en2lp  9069  tctr  9182  r1tr  9205  rankdmr1  9230  r1pw  9274  r1pwALT  9275  rankuni  9292  scottex  9314  cardidm  9388  alephcard  9496  alephnbtwn  9497  cfub  9671  cardcf  9674  cflecard  9675  cfle  9676  cflim2  9685  cfidm  9697  isf32lem9  9783  itunisuc  9841  itunitc1  9842  itunitc  9843  ituniiun  9844  axcc2lem  9858  alephreg  10004  pwcfsdom  10005  cfpwsdom  10006  axunndlem1  10017  axpownd  10023  tskmcl  10263  addcompi  10316  addasspi  10317  mulcompi  10318  mulasspi  10319  distrpi  10320  addnidpi  10323  nlt1pi  10328  addcompq  10372  addcomnq  10373  mulcompq  10374  mulcomnq  10375  adderpq  10378  mulerpq  10379  addassnq  10380  mulassnq  10381  distrnq  10383  genpass  10431  addcompr  10443  mulcompr  10445  distrpr  10450  ltexprlem7  10464  addcomsr  10509  addasssr  10510  mulcomsr  10511  mulasssr  10512  distrsr  10513  uzssz  12265  uzwo  12312  nn01to3  12342  xnn0xaddcl  12629  elixx3g  12752  iooid  12767  elfz2  12900  injresinjlem  13158  injresinj  13159  fleqceilz  13223  modifeq2int  13302  modfzo0difsn  13312  addmodlteq  13315  ltweuz  13330  fzofi  13343  fsuppmapnn0fiubex  13361  hashrabrsn  13734  hashrabsn01  13735  hashrabsn1  13736  elprchashprn2  13758  hashss  13771  hashsn01  13778  hash1snb  13781  hashgt12el  13784  hashgt12el2  13785  hashgt23el  13786  hashfzp1  13793  hash2pwpr  13835  hashge2el2dif  13839  ffz0iswrd  13891  ccatsymb  13936  swrd00  14006  swrd0  14020  swrdwrdsymb  14024  pfx00  14036  pfx0  14037  repswswrd  14146  0csh0  14155  cshwcl  14160  cshwidxmod  14165  repswcshw  14174  cshw1  14184  s3sndisj  14327  s3iunsndisj  14328  xptrrel  14340  trclfvcotrg  14376  relexpfld  14408  reusq0  14822  modfsummods  15148  pwm1geoserOLD  15225  dvdsaddre2b  15657  gcdaddmlem  15872  prm23ge5  16152  pcmptcl  16227  prmgaplem5  16391  prmgaplem6  16392  cshwshash  16438  strfvss  16506  strfvi  16537  setsnid  16539  ressbas  16554  ressbasss  16556  resslem  16557  ress0  16558  ressress  16562  strle1  16592  0rest  16703  firest  16706  topnval  16708  xpsaddlem  16846  xpsvsca  16850  homffval  16960  comfffval  16968  oppchomfval  16984  oppcbas  16988  fullfunc  17176  fthfunc  17177  natfval  17216  fucbas  17230  fuchom  17231  arwval  17303  coafval  17324  xpcbas  17428  xpchomfval  17429  xpccofval  17432  lubfun  17590  glbfun  17603  oduval  17740  oduleval  17741  odumeet  17750  odujoin  17752  ipopos  17770  plusffval  17858  grpidval  17871  gsum0  17894  frmdplusg  18019  frmd0  18025  efmndbas  18036  efmndbasabf  18037  efmndplusg  18045  mgm2nsgrplem2  18084  mgm2nsgrplem3  18085  sgrp2rid2  18091  dfgrp2e  18129  grpinvfval  18142  grpinvfvalALT  18143  grpinvfvi  18146  grpsubfval  18147  grpsubfvalALT  18148  mulgfval  18226  mulgfvalALT  18227  mulgfvi  18230  cntrval  18449  oppgval  18475  oppgplusfval  18476  symgval  18497  symgplusg  18511  snsymgefmndeq  18523  psgnfval  18628  odfval  18660  odfvalALT  18661  oppglsm  18767  efgval  18843  mgpval  19242  mgpplusg  19243  ringidval  19253  opprval  19374  opprmulfval  19375  dvdsrval  19395  invrfval  19423  dvrfval  19434  staffval  19618  scaffval  19652  rlmval  19963  rlmsca2  19973  2idlval  20006  rrgval  20060  asclfval  20108  psrplusg  20161  psrmulr  20164  psrvscafval  20170  mplval  20208  mplcoe3  20247  evlval  20308  psr1val  20354  vr1val  20360  ply1val  20362  ply1basfvi  20409  ply1plusgfvi  20410  psr1sca2  20419  ply1sca2  20422  ply1ascl  20426  cply1mul  20462  gsummoncoe1  20472  evl1fval  20491  evl1fval1  20494  zrhval  20655  zlmlem  20664  zlmvsca  20669  chrval  20672  evpmss  20730  psgndiflemB  20744  ipffval  20792  thlbas  20840  thlle  20841  thloc  20843  pjfval  20850  dsmmval2  20880  mamufacex  21000  mavmulsolcl  21160  marrepfval  21169  marepvfval  21174  submafval  21188  mdetfval  21195  mdetfval1  21199  mdetunilem7  21227  mdetunilem8  21228  madufval  21246  minmar1fval  21255  mp2pm2mplem4  21417  toponsspwpw  21530  tgdif0  21600  indislem  21608  resstopn  21794  iocpnfordt  21823  icomnfordt  21824  hmeofval  22366  ussval  22868  nmfval  23198  nghmfval  23331  pcofval  23614  tcphval  23821  ioombl  24166  ibladdlem  24420  itgaddlem1  24423  iblabs  24429  dvbsss  24500  perfdvf  24501  mdegfval  24656  deg1fval  24674  deg1fvi  24679  uc1pval  24733  mon1pval  24735  2irrexpq  25313  lgsqrmodndvds  25929  gausslemma2dlem1a  25941  2lgs  25983  2sqreultblem  26024  2sqreunnltblem  26027  ttglem  26662  axcontlem12  26761  vtxval  26785  iedgval  26786  edgval  26834  usgr1v  27038  nbuhgr  27125  nbumgr  27129  uhgrnbgr0nb  27136  nbgr1vtx  27140  nbgrnself2  27142  nbusgrvtxm1  27161  sizusglecusg  27245  g0wlk0  27433  wlkreslem  27451  lfgrwlkprop  27469  wwlks  27613  wwlksn  27615  wspthsn  27626  iswwlksnon  27631  iswspthsnon  27634  0enwwlksnge1  27642  wwlksnfi  27684  wwlksnfiOLD  27685  clwwlk  27761  umgrclwwlkge2  27769  clwlkclwwlklem2a4  27775  clwwlkn  27804  clwwlknfiOLD  27824  clwwlknonmpo  27868  clwwlknon  27869  clwwlk0on0  27871  clwwlknon1le1  27880  1conngr  27973  eupth2lem3lem7  28013  frgr1v  28050  nfrgr2v  28051  1to2vfriswmgr  28058  2wspmdisj  28116  frgrreggt1  28172  frgrreg  28173  frgrregord013  28174  frgrogt3nreg  28176  friendship  28178  avril1  28242  vafval  28380  bafval  28381  smfval  28382  vsfval  28410  bcsiALT  28956  resvsca  30903  resvlem  30904  cntnevol  31487  signsw0glem  31823  bnj1189  32281  hashfundm  32354  fmlafvel  32632  gonan0  32639  satffun  32656  mvtval  32747  mexval  32749  mexval2  32750  mdvval  32751  mrsubfval  32755  mrsubrn  32760  msubfval  32771  elmsubrn  32775  msubrn  32776  mvhfval  32780  mpstval  32782  msrfval  32784  mstaval  32791  mppsval  32819  mthmval  32822  dfrdg3  33041  trpredlem1  33066  fvsingle  33381  unisnif  33386  funpartfv  33406  fullfunfv  33408  linedegen  33604  bj-ax6e  34001  axc11n11r  34017  bj-ax12v3ALT  34020  bj-dtru  34139  bj-sbsb  34160  bj-nfcsym  34218  bj-restsnid  34381  bj-inftyexpitaudisj  34490  bj-inftyexpidisj  34495  csbdif  34609  finxpreclem4  34678  finxp00  34686  isinf2  34689  wl-nfs1t  34792  matunitlindflem1  34903  itg2addnclem  34958  ibladdnclem  34963  itgaddnclem1  34965  iblabsnc  34971  iblmulc2nc  34972  ftc1anclem8  34989  ismgmOLD  35143  tsbi1  35426  tsbi2  35427  ac6s6  35465  equid1  36050  ax12fromc15  36056  equid1ALT  36076  dvelimf-o  36080  ax12inda2ALT  36097  ax12inda2  36098  sn-axprlem3  39158  sn-dtru  39160  mzpmfp  39393  itgocn  39813  mendbas  39833  mendplusgfval  39834  mendmulrfval  39836  mendsca  39838  mendvscafval  39839  arearect  39871  areaquad  39872  sn1dom  39941  or3or  40420  uneqsn  40422  addcomgi  40837  ax6e2ndeq  40942  2sb5ndVD  41293  2sb5ndALT  41315  sqwvfoura  42562  sqwvfourb  42563  fourierswlem  42564  fouriersw  42565  hspdifhsp  42947  hspmbllem2  42958  hspmbl  42960  tz6.12-afv  43421  ndmaovcl  43451  tz6.12-afv2  43488  otiunsndisjX  43527  fvmptrab  43540  nltle2tri  43562  fzopredsuc  43572  iccpartiltu  43631  iccpartigtl  43632  iccpartlt  43633  icceuelpartlem  43644  iccpartnel  43647  elsprel  43686  sprssspr  43692  sprsymrelfvlem  43701  prprelprb  43728  prprspr2  43729  fmtnoprmfac1  43776  fmtnoprmfac2  43778  prmdvdsfmtnof1lem2  43796  prminf2  43799  lighneallem4  43824  requad1  43836  requad2  43837  evenprm2  43928  even3prm2  43933  fpprbasnn  43943  stgoldbwt  43990  upwlkbprop  44062  nzerooringczr  44392  pgrpgt2nabl  44463  suppmptcfin  44476  linc1  44529  lindslinindsimp2lem5  44566  reorelicc  44746  rrxsphere  44784  setrec2lem1  44845