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 ⊢ 𝜓

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.65iOLD  197  pm5.21nii  381  pm5.18  384  biass  388  pm2.61ian  823  ecase3  1048  4cases  1056  pm4.42  1069  ifpid  1093  elimh  1099  3ecase  1505  norass  1567  ax6e  2415  ax12  2455  exdistrf  2479  equvini  2487  ax12vALT  2501  2ax6e  2503  sb1  2510  sb2  2511  sb4a  2512  dfsb1  2513  dfsb2  2525  sbcom3  2538  sbco2  2543  sbco3  2545  sb9  2551  eujustALT  2600  pm2.61ine  3041  ralcom2  3366  eueq2  3673  moeq3  3675  mo2icl  3677  sbc2or  3753  unineq  4241  csb0  4375  sbcel12  4376  sbcne12  4380  sbcel2  4383  csbidm  4398  csbun  4406  csbin  4407  csbdif  4486  ifsb  4501  ifid  4528  ifnot  4540  ifan  4541  ifor  4542  csbif  4545  elimhyp  4553  elimhyp2v  4554  elimhyp3v  4555  elimhyp4v  4556  elimdhyp  4558  keephyp2v  4560  keephyp3v  4561  rmosn  4685  rabsnif  4689  tppreqb  4773  ssunsn2  4793  n0snor2el  4798  preq12nebg  4828  opthprneg  4830  elpreqprlem  4831  dfopif  4835  csbuni  4903  disjord  5098  sbcbr  5166  unisn2  5275  intabs  5319  class2set  5325  dtruALT2  5341  snexALT  5354  dtruALT  5359  axprlem3  5396  axprlem3OLD  5400  axprglem  5407  axprg  5408  snexOLD  5413  exneq  5417  copsexgwOLD  5473  copsexg  5474  snopeqop  5489  csbopab  5540  dfid3  5559  csbxp  5762  csbcnv  5872  csbres  5981  csbima12  6081  soirri  6126  csbrn  6204  dmsnopss  6215  dmsnsnsn  6221  opswap  6230  unixpid  6285  predres  6340  nsuceq0  6446  ordsssuc2  6454  iotassuni  6511  iotaex  6512  csbiota  6529  dffv3  6877  fvrn0  6909  ndmfv  6913  elfv2ex  6924  fveqres  6925  csbfv12  6926  csbfv  6928  dffv2  6976  fvco4i  6983  fvmptss  7002  fvmptex  7004  fvmptss2  7016  fvmptrabfv  7022  f0cli  7093  fvunsn  7177  fconst5  7204  csbriota  7382  riotassuni  7407  oprabidw  7441  csbov123  7454  csbov  7455  fvmptopab  7465  brfvopab  7467  elimdelov  7506  ovif12  7510  ifmpt2v  7512  ndmovcl  7595  ndmovord  7600  elovmpt3imp  7667  difsnexi  7756  ordsuc  7806  ordsucelsuc  7814  1stval  7984  2ndval  7985  1st2val  8010  2nd2val  8011  el2mpocsbcl  8076  bropopvvv  8081  bropfvvvvlem  8082  bropfvvvv  8083  suppimacnv  8166  suppssdm  8169  ressuppss  8175  suppun  8176  extmptsuppeq  8180  funsssuppss  8182  fczsupp0  8185  suppss  8186  suppss2  8192  suppssfv  8194  suppco  8198  mpoxopynvov0  8210  mpoxopoveqd  8213  pwuninelOLD  8268  smofvon2  8339  om0x  8500  mapssfset  8844  brdomg  8951  snfi  9036  sdomirr  9098  domunsn  9111  2pwuninel  9116  unfi  9151  cnvfi  9156  suppeqfsuppbi  9335  fsuppun  9343  funsnfsupp  9348  fipwuni  9382  oicl  9487  oif  9488  wemapso2  9511  card2on  9512  en2lp  9571  ttrclselem1  9690  tctr  9703  r1tr  9744  rankdmr1  9769  r1pw  9813  r1pwALT  9814  rankuni  9831  scottex  9855  cardidm  9941  alephcard  10050  alephnbtwn  10051  cfub  10227  cardcf  10230  cflecard  10231  cfle  10232  cflim2  10242  cfidm  10254  isf32lem9  10340  itunisuc  10398  itunitc1  10399  itunitc  10400  ituniiun  10401  axcc2lem  10415  alephreg  10562  pwcfsdom  10563  cfpwsdom  10564  axunndlem1  10575  axpownd  10581  tskmcl  10821  addcompi  10874  addasspi  10875  mulcompi  10876  mulasspi  10877  distrpi  10878  addnidpi  10881  nlt1pi  10886  addcompq  10930  addcomnq  10931  mulcompq  10932  mulcomnq  10933  adderpq  10936  mulerpq  10937  addassnq  10938  mulassnq  10939  distrnq  10941  genpass  10989  addcompr  11001  mulcompr  11003  distrpr  11008  ltexprlem7  11022  addcomsr  11067  addasssr  11068  mulcomsr  11069  mulasssr  11070  distrsr  11071  indval0  12217  uzssz  12878  uzwo  12930  nn01to3  12960  xnn0xaddcl  13256  elixx3g  13380  iooid  13395  elfz2  13537  injresinjlem  13815  injresinj  13816  fleqceilz  13883  modifeq2int  13965  modfzo0difsn  13975  addmodlteq  13978  ltweuz  13993  fzofi  14006  fsuppmapnn0fiubex  14024  hashrabrsn  14404  hashrabsn01  14405  hashrabsn1  14406  elprchashprn2  14428  hashss  14441  hashsn01  14449  hash1snb  14452  hashgt12el  14455  hashgt12el2  14456  hashgt23el  14457  hashfzp1  14464  hashfundm  14475  hash2pwpr  14509  hashge2el2dif  14513  hash3tpde  14526  ffz0iswrd  14574  ccatsymb  14616  swrd00  14678  swrd0  14692  swrdwrdsymb  14696  pfx00  14708  pfx0  14709  repswswrd  14817  0csh0  14826  cshwcl  14831  cshwidxmod  14836  repswcshw  14845  cshw1  14855  s3sndisj  15000  s3iunsndisj  15001  xptrrel  15013  trclfvcotrg  15049  relexpfld  15082  reusq0  15512  modfsummods  15841  dvdsaddre2b  16360  gcdaddmlem  16577  prm23ge5  16870  pcmptcl  16946  prmgaplem5  17110  prmgaplem6  17111  cshwshash  17159  strle1  17213  strfvss  17242  strfvi  17245  setsnid  17263  ressbas  17291  ressbasssg  17292  ressbasssOLD  17295  resseqnbas  17297  ress0  17298  ressress  17302  0rest  17477  firest  17480  topnval  17482  xpsaddlem  17622  xpsvsca  17626  homffval  17741  comfffval  17749  oppchomfval  17765  oppcbas  17769  fullfunc  17960  fthfunc  17961  natfval  18001  fucbas  18015  fuchom  18016  arwval  18095  coafval  18116  xpcbas  18229  xpchomfval  18230  xpccofval  18233  oduval  18339  oduleval  18340  lubfun  18401  glbfun  18414  odujoin  18457  odumeet  18459  ipopos  18587  plusffval  18699  grpidval  18714  gsum0  18737  frmdplusg  18908  frmd0  18914  efmndbas  18925  efmndbasabf  18926  efmndplusg  18934  mgm2nsgrplem2  18976  mgm2nsgrplem3  18977  sgrp2rid2  18983  dfgrp2e  19025  grpinvfval  19040  grpinvfvalALT  19041  grpinvfvi  19044  grpsubfval  19045  grpsubfvalALT  19046  mulgfval  19130  mulgfvalALT  19131  mulgfvi  19134  cntrval  19384  oppgval  19412  oppgplusfval  19413  symgval  19436  snsymgefmndeq  19460  psgnfval  19565  odfval  19597  odfvalALT  19598  oppglsm  19707  efgval  19782  mgpval  20214  mgpplusg  20215  ringidval  20260  opprval  20416  opprmulfval  20417  dvdsrval  20439  invrfval  20467  dvrfval  20480  rrgval  20796  staffval  20944  scaffval  21001  rlmval  21312  rlmsca2  21320  2idlval  21390  nzerooringczr  21630  zrhval  21657  zlmlem  21666  zlmvsca  21671  chrval  21673  evpmss  21736  psgndiflemB  21750  ipffval  21798  thlbas  21846  thlle  21847  thloc  21849  pjfval  21856  dsmmval2  21886  asclfval  22028  psrplusg  22087  psrmulr  22092  psrvscafval  22098  mplval  22138  mplcoe3  22189  evlval  22251  psr1val  22346  vr1val  22352  ply1val  22354  ply1basfvi  22400  ply1plusgfvi  22401  psr1sca2  22410  ply1sca2  22413  ply1ascl  22419  cply1mul  22456  gsummoncoe1  22468  evl1fval  22488  evl1fval1  22491  mamufacex  22553  mavmulsolcl  22708  marrepfval  22717  marepvfval  22722  submafval  22736  mdetfval  22743  mdetfval1  22747  mdetunilem7  22775  mdetunilem8  22776  madufval  22794  minmar1fval  22803  mp2pm2mplem4  22966  toponsspwpw  23079  tgdif0  23149  indislem  23157  resstopn  23343  iocpnfordt  23372  icomnfordt  23373  hmeofval  23915  ussval  24416  nmfval  24745  nghmfval  24879  pcofval  25169  tcphval  25377  ioombl  25724  ibladdlem  25979  itgaddlem1  25982  iblabs  25988  dvbsss  26061  perfdvf  26062  mdegfval  26219  deg1fval  26237  deg1fvi  26242  uc1pval  26297  mon1pval  26299  2irrexpq  26896  lgsqrmodndvds  27517  gausslemma2dlem1a  27529  2lgs  27571  2sqreultblem  27612  2sqreunnltblem  27615  newval  28028  leftval  28042  rightval  28043  lltr  28055  oldssmade  28060  oldss  28063  lrold  28090  ttglem  29225  axcontlem12  29325  vtxval  29350  iedgval  29351  edgval  29399  usgr1v  29606  nbuhgr  29693  nbumgr  29697  uhgrnbgr0nb  29704  nbgr1vtx  29708  nbgrnself2  29710  nbusgrvtxm1  29729  sizusglecusg  29813  g0wlk0  30000  wlkreslem  30017  lfgrwlkprop  30035  wwlks  30184  wwlksn  30186  wspthsn  30197  iswwlksnon  30202  iswspthsnon  30205  0enwwlksnge1  30213  wwlksnfi  30255  clwwlk  30334  umgrclwwlkge2  30342  clwlkclwwlklem2a4  30348  clwwlkn  30377  clwwlknonmpo  30440  clwwlknon  30441  clwwlk0on0  30443  clwwlknon1le1  30452  1conngr  30545  eupth2lem3lem7  30585  frgr1v  30622  nfrgr2v  30623  1to2vfriswmgr  30630  2wspmdisj  30688  frgrreggt1  30744  frgrreg  30745  frgrregord013  30746  frgrogt3nreg  30748  friendship  30750  avril1  30814  vafval  30955  bafval  30956  smfval  30957  vsfval  30985  bcsiALT  31531  of0r  33024  fracval  33625  fracbas  33626  resvsca  33652  resvlem  33653  cntnevol  34618  signsw0glem  34940  bnj1189  35397  r1wf  35489  rankscottu  35523  noinfepregs  35546  kardval  35565  kard0b  35572  kardcard2b  35578  rankkardu  35584  fmlafvel  35877  gonan0  35884  satffun  35901  mvtval  35992  mexval  35994  mexval2  35995  mdvval  35996  mrsubfval  36000  mrsubrn  36005  msubfval  36016  elmsubrn  36020  msubrn  36021  mvhfval  36025  mpstval  36027  msrfval  36029  mstaval  36036  mppsval  36064  mthmval  36067  antnestlaw2  36184  dfrdg3  36286  fvsingle  36410  unisnif  36415  funpartfv  36437  fullfunfv  36439  linedegen  36635  axtcond  36989  csbttc  37020  mh-setindnd  37048  bj-ax6e  37290  axc11n11r  37308  bj-ax12v3ALT  37311  bj-sbsb  37472  bj-nfcsym  37534  bj-snex  37671  bj-restsnid  37729  bj-inftyexpitaudisj  37849  bj-inftyexpidisj  37854  finxpreclem4  38040  finxp00  38048  isinf2  38051  wl-nfs1t  38192  matunitlindflem1  38267  itg2addnclem  38322  ibladdnclem  38327  itgaddnclem1  38329  iblabsnc  38335  iblmulc2nc  38336  ftc1anclem8  38351  ismgmOLD  38501  tsbi1  38782  tsbi2  38783  ac6s6  38821  equid1  39673  ax12fromc15  39679  equid1ALT  39699  dvelimf-o  39703  ax12inda2ALT  39720  ax12inda2  39721  sn-axprlem3  42989  fsuppind  43322  mzpmfp  43478  itgocn  43891  mendbas  43907  mendplusgfval  43908  mendmulrfval  43910  mendsca  43912  mendvscafval  43913  arearect  43942  areaquad  43943  fpwfvss  44138  safesnsupfidom1o  44143  sn1dom  44252  or3or  44749  uneqsn  44751  addcomgi  45164  ax6e2ndeq  45268  2sb5ndVD  45618  2sb5ndALT  45640  sqwvfoura  46942  sqwvfourb  46943  fourierswlem  46944  fouriersw  46945  hspdifhsp  47330  hspmbllem2  47341  hspmbl  47343  et-ltneverrefl  47585  tz6.12-afv  47910  ndmaovcl  47940  tz6.12-afv2  47977  otiunsndisjX  48016  fvmptrab  48029  nltle2tri  48050  fzopredsuc  48061  iccpartiltu  48171  iccpartigtl  48172  iccpartlt  48173  icceuelpartlem  48184  iccpartnel  48187  elsprel  48224  sprssspr  48230  sprsymrelfvlem  48239  prprelprb  48266  prprspr2  48267  fmtnoprmfac1  48317  fmtnoprmfac2  48319  prmdvdsfmtnof1lem2  48337  prminf2  48340  lighneallem4  48362  requad1  48387  requad2  48388  evenprm2  48479  even3prm2  48484  fpprbasnn  48494  stgoldbwt  48541  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  pgnbgreunbgrlem2lem3  48881  upwlkbprop  48903  pgrpgt2nabl  49146  suppmptcfin  49156  linc1  49205  lindslinindsimp2lem5  49242  1aryenef  49425  2aryenef  49436  reorelicc  49490  rrxsphere  49528  fvconst0ci  49669  fvconstdomi  49670  upfval  49954  reldmprcof1  50159  reldmprcof2  50160  lmdfval  50427  cmdfval  50428  setrec2lem1  50471  setrec2mpt  50475