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  2385  ax12  2425  exdistrf  2449  equvini  2457  ax12vALT  2471  2ax6e  2473  sb1  2480  sb2  2481  sb4a  2482  dfsb1  2483  dfsb2  2495  sbcom3  2508  sbco2  2513  sbco3  2515  sb9  2521  eujustALT  2570  pm2.61ine  3013  ralcom2  3345  eueq2  3666  moeq3  3668  mo2icl  3670  sbc2or  3747  unineq  4238  csb0  4360  sbcel12  4361  sbcne12  4365  sbcel2  4368  csbidm  4383  csbun  4391  csbin  4392  csbdif  4476  ifsb  4491  ifid  4518  ifnot  4530  ifan  4531  ifor  4532  csbif  4535  elimhyp  4543  elimhyp2v  4544  elimhyp3v  4545  elimhyp4v  4546  elimdhyp  4548  keephyp2v  4550  keephyp3v  4551  rmosn  4674  rabsnif  4678  tppreqb  4759  ssunsn2  4781  n0snor2el  4787  preq12nebg  4817  opthprneg  4819  elpreqprlem  4820  dfopif  4824  csbuni  4891  disjord  5085  sbcbr  5151  unisn2  5255  intabs  5292  class2set  5298  dtruALT2  5313  snexALT  5326  dtruALT  5331  axprlem3  5368  axprlem3OLD  5371  snex  5379  exneq  5383  copsexgw  5436  copsexg  5437  snopeqop  5452  csbopab  5501  dfid3  5520  csbxp  5723  csbres  5939  csbima12  6036  soirri  6081  csbrn  6159  dmsnopss  6170  dmsnsnsn  6176  opswap  6185  unixpid  6240  predres  6295  nsuceq0  6400  ordsssuc2  6408  iotassuni  6465  iotaex  6466  csbiota  6483  dffv3  6828  fvrn0  6860  ndmfv  6864  elfv2ex  6875  fveqres  6876  csbfv12  6877  csbfv  6879  dffv2  6927  fvco4i  6933  fvmptss  6951  fvmptex  6953  fvmptss2  6965  fvmptrabfv  6971  f0cli  7041  fvunsn  7123  fconst5  7150  csbriota  7328  riotassuni  7353  oprabidw  7387  csbov123  7400  csbov  7401  fvmptopab  7411  brfvopab  7413  elimdelov  7452  ovif12  7456  ifmpt2v  7458  ndmovcl  7541  ndmovord  7546  elovmpt3imp  7613  difsnexi  7704  ordsuc  7754  ordsucelsuc  7762  1stval  7933  2ndval  7934  1st2val  7959  2nd2val  7960  el2mpocsbcl  8025  bropopvvv  8030  bropfvvvvlem  8031  bropfvvvv  8032  suppimacnv  8114  suppssdm  8117  ressuppss  8123  suppun  8124  extmptsuppeq  8128  funsssuppss  8130  fczsupp0  8133  suppss  8134  suppss2  8140  suppssfv  8142  suppco  8146  mpoxopynvov0  8158  mpoxopoveqd  8161  pwuninel  8215  smofvon2  8286  om0x  8444  mapssfset  8786  brdomg  8893  snfi  8978  sdomirr  9040  domunsn  9053  2pwuninel  9058  unfi  9093  cnvfi  9098  suppeqfsuppbi  9280  fsuppun  9288  funsnfsupp  9293  fipwuni  9327  oicl  9432  oif  9433  wemapso2  9456  card2on  9457  en2lp  9513  ttrclselem1  9632  tctr  9645  r1tr  9686  rankdmr1  9711  r1pw  9755  r1pwALT  9756  rankuni  9773  scottex  9795  cardidm  9869  alephcard  9978  alephnbtwn  9979  cfub  10157  cardcf  10160  cflecard  10161  cfle  10162  cflim2  10171  cfidm  10183  isf32lem9  10269  itunisuc  10327  itunitc1  10328  itunitc  10329  ituniiun  10330  axcc2lem  10344  alephreg  10491  pwcfsdom  10492  cfpwsdom  10493  axunndlem1  10504  axpownd  10510  tskmcl  10750  addcompi  10803  addasspi  10804  mulcompi  10805  mulasspi  10806  distrpi  10807  addnidpi  10810  nlt1pi  10815  addcompq  10859  addcomnq  10860  mulcompq  10861  mulcomnq  10862  adderpq  10865  mulerpq  10866  addassnq  10867  mulassnq  10868  distrnq  10870  genpass  10918  addcompr  10930  mulcompr  10932  distrpr  10937  ltexprlem7  10951  addcomsr  10996  addasssr  10997  mulcomsr  10998  mulasssr  10999  distrsr  11000  uzssz  12770  uzwo  12822  nn01to3  12852  xnn0xaddcl  13148  elixx3g  13272  iooid  13287  elfz2  13428  injresinjlem  13704  injresinj  13705  fleqceilz  13772  modifeq2int  13854  modfzo0difsn  13864  addmodlteq  13867  ltweuz  13882  fzofi  13895  fsuppmapnn0fiubex  13913  hashrabrsn  14293  hashrabsn01  14294  hashrabsn1  14295  elprchashprn2  14317  hashss  14330  hashsn01  14337  hash1snb  14340  hashgt12el  14343  hashgt12el2  14344  hashgt23el  14345  hashfzp1  14352  hashfundm  14363  hash2pwpr  14397  hashge2el2dif  14401  hash3tpde  14414  ffz0iswrd  14462  ccatsymb  14504  swrd00  14566  swrd0  14580  swrdwrdsymb  14584  pfx00  14596  pfx0  14597  repswswrd  14705  0csh0  14714  cshwcl  14719  cshwidxmod  14724  repswcshw  14733  cshw1  14743  s3sndisj  14888  s3iunsndisj  14889  xptrrel  14901  trclfvcotrg  14937  relexpfld  14970  reusq0  15386  modfsummods  15714  dvdsaddre2b  16232  gcdaddmlem  16449  prm23ge5  16741  pcmptcl  16817  prmgaplem5  16981  prmgaplem6  16982  cshwshash  17030  strle1  17083  strfvss  17112  strfvi  17115  setsnid  17133  ressbas  17161  ressbasssg  17162  ressbasssOLD  17165  resseqnbas  17167  ress0  17168  ressress  17172  0rest  17347  firest  17350  topnval  17352  xpsaddlem  17492  xpsvsca  17496  homffval  17611  comfffval  17619  oppchomfval  17635  oppcbas  17639  fullfunc  17830  fthfunc  17831  natfval  17871  fucbas  17885  fuchom  17886  arwval  17965  coafval  17986  xpcbas  18099  xpchomfval  18100  xpccofval  18103  oduval  18209  oduleval  18210  lubfun  18271  glbfun  18284  odujoin  18327  odumeet  18329  ipopos  18457  plusffval  18569  grpidval  18584  gsum0  18607  frmdplusg  18777  frmd0  18783  efmndbas  18794  efmndbasabf  18795  efmndplusg  18803  mgm2nsgrplem2  18842  mgm2nsgrplem3  18843  sgrp2rid2  18849  dfgrp2e  18891  grpinvfval  18906  grpinvfvalALT  18907  grpinvfvi  18910  grpsubfval  18911  grpsubfvalALT  18912  mulgfval  18997  mulgfvalALT  18998  mulgfvi  19001  cntrval  19246  oppgval  19274  oppgplusfval  19275  symgval  19298  snsymgefmndeq  19322  psgnfval  19427  odfval  19459  odfvalALT  19460  oppglsm  19569  efgval  19644  mgpval  20076  mgpplusg  20077  ringidval  20116  opprval  20272  opprmulfval  20273  dvdsrval  20295  invrfval  20323  dvrfval  20336  rrgval  20628  staffval  20772  scaffval  20829  rlmval  21141  rlmsca2  21149  2idlval  21204  nzerooringczr  21433  zrhval  21460  zlmlem  21469  zlmvsca  21474  chrval  21476  evpmss  21539  psgndiflemB  21553  ipffval  21601  thlbas  21649  thlle  21650  thloc  21652  pjfval  21659  dsmmval2  21689  asclfval  21832  psrplusg  21890  psrmulr  21896  psrvscafval  21902  mplval  21942  mplcoe3  21991  evlval  22053  psr1val  22124  vr1val  22130  ply1val  22132  ply1basfvi  22179  ply1plusgfvi  22180  psr1sca2  22189  ply1sca2  22192  ply1ascl  22198  cply1mul  22238  gsummoncoe1  22250  evl1fval  22270  evl1fval1  22273  mamufacex  22338  mavmulsolcl  22493  marrepfval  22502  marepvfval  22507  submafval  22521  mdetfval  22528  mdetfval1  22532  mdetunilem7  22560  mdetunilem8  22561  madufval  22579  minmar1fval  22588  mp2pm2mplem4  22751  toponsspwpw  22864  tgdif0  22934  indislem  22942  resstopn  23128  iocpnfordt  23157  icomnfordt  23158  hmeofval  23700  ussval  24201  nmfval  24530  nghmfval  24664  pcofval  24964  tcphval  25172  ioombl  25520  ibladdlem  25775  itgaddlem1  25778  iblabs  25784  dvbsss  25857  perfdvf  25858  mdegfval  26021  deg1fval  26039  deg1fvi  26044  uc1pval  26099  mon1pval  26101  2irrexpq  26694  lgsqrmodndvds  27318  gausslemma2dlem1a  27330  2lgs  27372  2sqreultblem  27413  2sqreunnltblem  27416  newval  27823  leftval  27831  rightval  27832  lltropt  27844  oldssmade  27849  oldss  27850  lrold  27869  ttglem  28897  axcontlem12  28997  vtxval  29022  iedgval  29023  edgval  29071  usgr1v  29278  nbuhgr  29365  nbumgr  29369  uhgrnbgr0nb  29376  nbgr1vtx  29380  nbgrnself2  29382  nbusgrvtxm1  29401  sizusglecusg  29486  g0wlk0  29673  wlkreslem  29690  lfgrwlkprop  29708  wwlks  29857  wwlksn  29859  wspthsn  29870  iswwlksnon  29875  iswspthsnon  29878  0enwwlksnge1  29886  wwlksnfi  29928  clwwlk  30007  umgrclwwlkge2  30015  clwlkclwwlklem2a4  30021  clwwlkn  30050  clwwlknonmpo  30113  clwwlknon  30114  clwwlk0on0  30116  clwwlknon1le1  30125  1conngr  30218  eupth2lem3lem7  30258  frgr1v  30295  nfrgr2v  30296  1to2vfriswmgr  30303  2wspmdisj  30361  frgrreggt1  30417  frgrreg  30418  frgrregord013  30419  frgrogt3nreg  30421  friendship  30423  avril1  30487  vafval  30627  bafval  30628  smfval  30629  vsfval  30657  bcsiALT  31203  of0r  32707  fracval  33335  fracbas  33336  resvsca  33362  resvlem  33363  cntnevol  34334  signsw0glem  34659  bnj1189  35114  r1wf  35201  noinfepregs  35238  fmlafvel  35528  gonan0  35535  satffun  35552  mvtval  35643  mexval  35645  mexval2  35646  mdvval  35647  mrsubfval  35651  mrsubrn  35656  msubfval  35667  elmsubrn  35671  msubrn  35672  mvhfval  35676  mpstval  35678  msrfval  35680  mstaval  35687  mppsval  35715  mthmval  35718  antnestlaw2  35835  dfrdg3  35937  fvsingle  36061  unisnif  36066  funpartfv  36088  fullfunfv  36090  linedegen  36286  bj-ax6e  36812  axc11n11r  36827  bj-ax12v3ALT  36830  bj-sbsb  36981  bj-nfcsym  37043  bj-snex  37179  bj-restsnid  37231  bj-inftyexpitaudisj  37349  bj-inftyexpidisj  37354  finxpreclem4  37538  finxp00  37546  isinf2  37549  wl-nfs1t  37681  matunitlindflem1  37756  itg2addnclem  37811  ibladdnclem  37816  itgaddnclem1  37818  iblabsnc  37824  iblmulc2nc  37825  ftc1anclem8  37840  ismgmOLD  37990  tsbi1  38273  tsbi2  38274  ac6s6  38312  equid1  39098  ax12fromc15  39104  equid1ALT  39124  dvelimf-o  39128  ax12inda2ALT  39145  ax12inda2  39146  sn-axprlem3  42415  fsuppind  42775  mzpmfp  42931  itgocn  43348  mendbas  43364  mendplusgfval  43365  mendmulrfval  43367  mendsca  43369  mendvscafval  43370  arearect  43399  areaquad  43400  fpwfvss  43595  safesnsupfidom1o  43600  sn1dom  43709  or3or  44206  uneqsn  44208  addcomgi  44638  ax6e2ndeq  44742  2sb5ndVD  45092  2sb5ndALT  45114  sqwvfoura  46414  sqwvfourb  46415  fourierswlem  46416  fouriersw  46417  hspdifhsp  46802  hspmbllem2  46813  hspmbl  46815  et-ltneverrefl  47057  tz6.12-afv  47361  ndmaovcl  47391  tz6.12-afv2  47428  otiunsndisjX  47467  fvmptrab  47480  nltle2tri  47501  fzopredsuc  47511  iccpartiltu  47610  iccpartigtl  47611  iccpartlt  47612  icceuelpartlem  47623  iccpartnel  47626  elsprel  47663  sprssspr  47669  sprsymrelfvlem  47678  prprelprb  47705  prprspr2  47706  fmtnoprmfac1  47753  fmtnoprmfac2  47755  prmdvdsfmtnof1lem2  47773  prminf2  47776  lighneallem4  47798  requad1  47810  requad2  47811  evenprm2  47902  even3prm2  47907  fpprbasnn  47917  stgoldbwt  47964  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  upwlkbprop  48326  pgrpgt2nabl  48554  suppmptcfin  48564  linc1  48613  lindslinindsimp2lem5  48650  1aryenef  48833  2aryenef  48844  reorelicc  48898  rrxsphere  48936  fvconst0ci  49078  fvconstdomi  49079  upfval  49363  reldmprcof1  49568  reldmprcof2  49569  lmdfval  49836  cmdfval  49837  setrec2lem1  49880  setrec2mpt  49884