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  1538  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  2572  pm2.61ine  3015  ralcom2  3347  eueq2  3668  moeq3  3670  mo2icl  3672  sbc2or  3749  unineq  4240  csb0  4362  sbcel12  4363  sbcne12  4367  sbcel2  4370  csbidm  4385  csbun  4393  csbin  4394  csbdif  4478  ifsb  4493  ifid  4520  ifnot  4532  ifan  4533  ifor  4534  csbif  4537  elimhyp  4545  elimhyp2v  4546  elimhyp3v  4547  elimhyp4v  4548  elimdhyp  4550  keephyp2v  4552  keephyp3v  4553  rmosn  4676  rabsnif  4680  tppreqb  4761  ssunsn2  4783  n0snor2el  4789  preq12nebg  4819  opthprneg  4821  elpreqprlem  4822  dfopif  4826  csbuni  4893  disjord  5087  sbcbr  5153  unisn2  5257  intabs  5294  class2set  5300  dtruALT2  5315  snexALT  5328  dtruALT  5333  axprlem3  5370  axprlem3OLD  5373  snex  5381  exneq  5385  copsexgw  5438  copsexg  5439  snopeqop  5454  csbopab  5503  dfid3  5522  csbxp  5725  csbres  5941  csbima12  6038  soirri  6083  csbrn  6161  dmsnopss  6172  dmsnsnsn  6178  opswap  6187  unixpid  6242  predres  6297  nsuceq0  6402  ordsssuc2  6410  iotassuni  6467  iotaex  6468  csbiota  6485  dffv3  6830  fvrn0  6862  ndmfv  6866  elfv2ex  6877  fveqres  6878  csbfv12  6879  csbfv  6881  dffv2  6929  fvco4i  6935  fvmptss  6953  fvmptex  6955  fvmptss2  6967  fvmptrabfv  6973  f0cli  7043  fvunsn  7125  fconst5  7152  csbriota  7330  riotassuni  7355  oprabidw  7389  csbov123  7402  csbov  7403  fvmptopab  7413  brfvopab  7415  elimdelov  7454  ovif12  7458  ifmpt2v  7460  ndmovcl  7543  ndmovord  7548  elovmpt3imp  7615  difsnexi  7706  ordsuc  7756  ordsucelsuc  7764  1stval  7935  2ndval  7936  1st2val  7961  2nd2val  7962  el2mpocsbcl  8027  bropopvvv  8032  bropfvvvvlem  8033  bropfvvvv  8034  suppimacnv  8116  suppssdm  8119  ressuppss  8125  suppun  8126  extmptsuppeq  8130  funsssuppss  8132  fczsupp0  8135  suppss  8136  suppss2  8142  suppssfv  8144  suppco  8148  mpoxopynvov0  8160  mpoxopoveqd  8163  pwuninel  8217  smofvon2  8288  om0x  8446  mapssfset  8788  brdomg  8895  snfi  8980  sdomirr  9042  domunsn  9055  2pwuninel  9060  unfi  9095  cnvfi  9100  suppeqfsuppbi  9282  fsuppun  9290  funsnfsupp  9295  fipwuni  9329  oicl  9434  oif  9435  wemapso2  9458  card2on  9459  en2lp  9515  ttrclselem1  9634  tctr  9647  r1tr  9688  rankdmr1  9713  r1pw  9757  r1pwALT  9758  rankuni  9775  scottex  9797  cardidm  9871  alephcard  9980  alephnbtwn  9981  cfub  10159  cardcf  10162  cflecard  10163  cfle  10164  cflim2  10173  cfidm  10185  isf32lem9  10271  itunisuc  10329  itunitc1  10330  itunitc  10331  ituniiun  10332  axcc2lem  10346  alephreg  10493  pwcfsdom  10494  cfpwsdom  10495  axunndlem1  10506  axpownd  10512  tskmcl  10752  addcompi  10805  addasspi  10806  mulcompi  10807  mulasspi  10808  distrpi  10809  addnidpi  10812  nlt1pi  10817  addcompq  10861  addcomnq  10862  mulcompq  10863  mulcomnq  10864  adderpq  10867  mulerpq  10868  addassnq  10869  mulassnq  10870  distrnq  10872  genpass  10920  addcompr  10932  mulcompr  10934  distrpr  10939  ltexprlem7  10953  addcomsr  10998  addasssr  10999  mulcomsr  11000  mulasssr  11001  distrsr  11002  uzssz  12772  uzwo  12824  nn01to3  12854  xnn0xaddcl  13150  elixx3g  13274  iooid  13289  elfz2  13430  injresinjlem  13706  injresinj  13707  fleqceilz  13774  modifeq2int  13856  modfzo0difsn  13866  addmodlteq  13869  ltweuz  13884  fzofi  13897  fsuppmapnn0fiubex  13915  hashrabrsn  14295  hashrabsn01  14296  hashrabsn1  14297  elprchashprn2  14319  hashss  14332  hashsn01  14339  hash1snb  14342  hashgt12el  14345  hashgt12el2  14346  hashgt23el  14347  hashfzp1  14354  hashfundm  14365  hash2pwpr  14399  hashge2el2dif  14403  hash3tpde  14416  ffz0iswrd  14464  ccatsymb  14506  swrd00  14568  swrd0  14582  swrdwrdsymb  14586  pfx00  14598  pfx0  14599  repswswrd  14707  0csh0  14716  cshwcl  14721  cshwidxmod  14726  repswcshw  14735  cshw1  14745  s3sndisj  14890  s3iunsndisj  14891  xptrrel  14903  trclfvcotrg  14939  relexpfld  14972  reusq0  15388  modfsummods  15716  dvdsaddre2b  16234  gcdaddmlem  16451  prm23ge5  16743  pcmptcl  16819  prmgaplem5  16983  prmgaplem6  16984  cshwshash  17032  strle1  17085  strfvss  17114  strfvi  17117  setsnid  17135  ressbas  17163  ressbasssg  17164  ressbasssOLD  17167  resseqnbas  17169  ress0  17170  ressress  17174  0rest  17349  firest  17352  topnval  17354  xpsaddlem  17494  xpsvsca  17498  homffval  17613  comfffval  17621  oppchomfval  17637  oppcbas  17641  fullfunc  17832  fthfunc  17833  natfval  17873  fucbas  17887  fuchom  17888  arwval  17967  coafval  17988  xpcbas  18101  xpchomfval  18102  xpccofval  18105  oduval  18211  oduleval  18212  lubfun  18273  glbfun  18286  odujoin  18329  odumeet  18331  ipopos  18459  plusffval  18571  grpidval  18586  gsum0  18609  frmdplusg  18779  frmd0  18785  efmndbas  18796  efmndbasabf  18797  efmndplusg  18805  mgm2nsgrplem2  18844  mgm2nsgrplem3  18845  sgrp2rid2  18851  dfgrp2e  18893  grpinvfval  18908  grpinvfvalALT  18909  grpinvfvi  18912  grpsubfval  18913  grpsubfvalALT  18914  mulgfval  18999  mulgfvalALT  19000  mulgfvi  19003  cntrval  19248  oppgval  19276  oppgplusfval  19277  symgval  19300  snsymgefmndeq  19324  psgnfval  19429  odfval  19461  odfvalALT  19462  oppglsm  19571  efgval  19646  mgpval  20078  mgpplusg  20079  ringidval  20118  opprval  20274  opprmulfval  20275  dvdsrval  20297  invrfval  20325  dvrfval  20338  rrgval  20630  staffval  20774  scaffval  20831  rlmval  21143  rlmsca2  21151  2idlval  21206  nzerooringczr  21435  zrhval  21462  zlmlem  21471  zlmvsca  21476  chrval  21478  evpmss  21541  psgndiflemB  21555  ipffval  21603  thlbas  21651  thlle  21652  thloc  21654  pjfval  21661  dsmmval2  21691  asclfval  21834  psrplusg  21892  psrmulr  21898  psrvscafval  21904  mplval  21944  mplcoe3  21993  evlval  22055  psr1val  22126  vr1val  22132  ply1val  22134  ply1basfvi  22181  ply1plusgfvi  22182  psr1sca2  22191  ply1sca2  22194  ply1ascl  22200  cply1mul  22240  gsummoncoe1  22252  evl1fval  22272  evl1fval1  22275  mamufacex  22340  mavmulsolcl  22495  marrepfval  22504  marepvfval  22509  submafval  22523  mdetfval  22530  mdetfval1  22534  mdetunilem7  22562  mdetunilem8  22563  madufval  22581  minmar1fval  22590  mp2pm2mplem4  22753  toponsspwpw  22866  tgdif0  22936  indislem  22944  resstopn  23130  iocpnfordt  23159  icomnfordt  23160  hmeofval  23702  ussval  24203  nmfval  24532  nghmfval  24666  pcofval  24966  tcphval  25174  ioombl  25522  ibladdlem  25777  itgaddlem1  25780  iblabs  25786  dvbsss  25859  perfdvf  25860  mdegfval  26023  deg1fval  26041  deg1fvi  26046  uc1pval  26101  mon1pval  26103  2irrexpq  26696  lgsqrmodndvds  27320  gausslemma2dlem1a  27332  2lgs  27374  2sqreultblem  27415  2sqreunnltblem  27418  newval  27831  leftval  27845  rightval  27846  lltr  27858  oldssmade  27863  oldss  27866  lrold  27893  ttglem  28948  axcontlem12  29048  vtxval  29073  iedgval  29074  edgval  29122  usgr1v  29329  nbuhgr  29416  nbumgr  29420  uhgrnbgr0nb  29427  nbgr1vtx  29431  nbgrnself2  29433  nbusgrvtxm1  29452  sizusglecusg  29537  g0wlk0  29724  wlkreslem  29741  lfgrwlkprop  29759  wwlks  29908  wwlksn  29910  wspthsn  29921  iswwlksnon  29926  iswspthsnon  29929  0enwwlksnge1  29937  wwlksnfi  29979  clwwlk  30058  umgrclwwlkge2  30066  clwlkclwwlklem2a4  30072  clwwlkn  30101  clwwlknonmpo  30164  clwwlknon  30165  clwwlk0on0  30167  clwwlknon1le1  30176  1conngr  30269  eupth2lem3lem7  30309  frgr1v  30346  nfrgr2v  30347  1to2vfriswmgr  30354  2wspmdisj  30412  frgrreggt1  30468  frgrreg  30469  frgrregord013  30470  frgrogt3nreg  30472  friendship  30474  avril1  30538  vafval  30678  bafval  30679  smfval  30680  vsfval  30708  bcsiALT  31254  of0r  32758  fracval  33386  fracbas  33387  resvsca  33413  resvlem  33414  cntnevol  34385  signsw0glem  34710  bnj1189  35165  r1wf  35252  noinfepregs  35289  fmlafvel  35579  gonan0  35586  satffun  35603  mvtval  35694  mexval  35696  mexval2  35697  mdvval  35698  mrsubfval  35702  mrsubrn  35707  msubfval  35718  elmsubrn  35722  msubrn  35723  mvhfval  35727  mpstval  35729  msrfval  35731  mstaval  35738  mppsval  35766  mthmval  35769  antnestlaw2  35886  dfrdg3  35988  fvsingle  36112  unisnif  36117  funpartfv  36139  fullfunfv  36141  linedegen  36337  mh-setindnd  36667  bj-ax6e  36869  axc11n11r  36884  bj-ax12v3ALT  36887  bj-sbsb  37038  bj-nfcsym  37100  bj-snex  37236  bj-restsnid  37292  bj-inftyexpitaudisj  37410  bj-inftyexpidisj  37415  finxpreclem4  37599  finxp00  37607  isinf2  37610  wl-nfs1t  37742  matunitlindflem1  37817  itg2addnclem  37872  ibladdnclem  37877  itgaddnclem1  37879  iblabsnc  37885  iblmulc2nc  37886  ftc1anclem8  37901  ismgmOLD  38051  tsbi1  38334  tsbi2  38335  ac6s6  38373  equid1  39159  ax12fromc15  39165  equid1ALT  39185  dvelimf-o  39189  ax12inda2ALT  39206  ax12inda2  39207  sn-axprlem3  42474  fsuppind  42833  mzpmfp  42989  itgocn  43406  mendbas  43422  mendplusgfval  43423  mendmulrfval  43425  mendsca  43427  mendvscafval  43428  arearect  43457  areaquad  43458  fpwfvss  43653  safesnsupfidom1o  43658  sn1dom  43767  or3or  44264  uneqsn  44266  addcomgi  44696  ax6e2ndeq  44800  2sb5ndVD  45150  2sb5ndALT  45172  sqwvfoura  46472  sqwvfourb  46473  fourierswlem  46474  fouriersw  46475  hspdifhsp  46860  hspmbllem2  46871  hspmbl  46873  et-ltneverrefl  47115  tz6.12-afv  47419  ndmaovcl  47449  tz6.12-afv2  47486  otiunsndisjX  47525  fvmptrab  47538  nltle2tri  47559  fzopredsuc  47569  iccpartiltu  47668  iccpartigtl  47669  iccpartlt  47670  icceuelpartlem  47681  iccpartnel  47684  elsprel  47721  sprssspr  47727  sprsymrelfvlem  47736  prprelprb  47763  prprspr2  47764  fmtnoprmfac1  47811  fmtnoprmfac2  47813  prmdvdsfmtnof1lem2  47831  prminf2  47834  lighneallem4  47856  requad1  47868  requad2  47869  evenprm2  47960  even3prm2  47965  fpprbasnn  47975  stgoldbwt  48022  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  upwlkbprop  48384  pgrpgt2nabl  48612  suppmptcfin  48622  linc1  48671  lindslinindsimp2lem5  48708  1aryenef  48891  2aryenef  48902  reorelicc  48956  rrxsphere  48994  fvconst0ci  49136  fvconstdomi  49137  upfval  49421  reldmprcof1  49626  reldmprcof2  49627  lmdfval  49894  cmdfval  49895  setrec2lem1  49938  setrec2mpt  49942