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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.61ii  185  pm2.61nii  186  pm2.61iii  187  pm2.65iOLD  197  pm5.21nii  381  pm5.18  384  biass  388  pm2.61ian  824  ecase3  1048  4cases  1056  pm4.42  1069  ifpid  1093  elimh  1099  3ecase  1505  norass  1567  ax6e  2417  ax12  2457  exdistrf  2481  equvini  2489  ax12vALT  2503  2ax6e  2505  sb1  2512  sb2  2513  sb4a  2514  dfsb1  2515  dfsb2  2527  sbcom3  2540  sbco2  2545  sbco3  2547  sb9  2553  eujustALT  2602  pm2.61ine  3043  ralcom2  3368  eueq2  3675  moeq3  3677  mo2icl  3679  sbc2or  3755  unineq  4241  csb0  4375  sbcel12  4376  sbcne12  4380  sbcel2  4383  csbidm  4398  csbun  4406  csbin  4407  csbdif  4488  ifsb  4503  ifid  4530  ifnot  4542  ifan  4543  ifor  4544  csbif  4547  elimhyp  4555  elimhyp2v  4556  elimhyp3v  4557  elimhyp4v  4558  elimdhyp  4560  keephyp2v  4562  keephyp3v  4563  rmosn  4687  rabsnif  4691  tppreqb  4775  ssunsn2  4795  n0snor2el  4800  preq12nebg  4830  opthprneg  4832  elpreqprlem  4833  dfopif  4837  csbuni  4905  disjord  5100  sbcbr  5168  unisn2  5277  intabs  5321  class2set  5327  dtruALT2  5343  snexALT  5356  dtruALT  5361  axprlem3  5398  axprlem3OLD  5402  axprglem  5409  axprg  5410  snexOLD  5415  exneq  5419  copsexgwOLD  5475  copsexg  5476  snopeqop  5491  csbopab  5542  dfid3  5561  csbxp  5764  csbcnv  5874  csbres  5983  csbima12  6083  soirri  6128  csbrn  6206  dmsnopss  6217  dmsnsnsn  6223  opswap  6232  unixpid  6289  predres  6344  nsuceq0  6450  ordsssuc2  6458  iotassuni  6515  iotaex  6516  csbiota  6533  dffv3  6881  fvrn0  6913  ndmfv  6917  elfv2ex  6928  fveqres  6929  csbfv12  6930  csbfv  6932  dffv2  6980  fvco4i  6987  fvmptss  7006  fvmptex  7008  fvmptss2  7020  fvmptrabfv  7026  f0cli  7097  fvunsn  7183  fconst5  7211  csbriota  7391  riotassuni  7416  oprabidw  7450  csbov123  7463  csbov  7464  fvmptopab  7474  brfvopab  7476  elimdelov  7515  ovif12  7519  ifmpt2v  7521  ndmovcl  7605  ndmovord  7610  elovmpt3imp  7677  difsnexi  7766  ordsuc  7816  ordsucelsuc  7824  1stval  7994  2ndval  7995  1st2val  8020  2nd2val  8021  el2mpocsbcl  8086  bropopvvv  8091  bropfvvvvlem  8092  bropfvvvv  8093  suppimacnv  8176  suppssdm  8179  ressuppss  8185  suppun  8186  extmptsuppeq  8190  funsssuppss  8192  fczsupp0  8195  suppss  8196  suppss2  8202  suppssfv  8204  suppco  8208  mpoxopynvov0  8220  mpoxopoveqd  8223  pwuninelOLD  8278  smofvon2  8349  om0x  8510  mapssfset  8854  brdomg  8961  snfi  9047  sdomirr  9109  domunsn  9122  2pwuninel  9127  unfi  9162  cnvfi  9167  suppeqfsuppbi  9346  fsuppun  9354  funsnfsupp  9359  fipwuni  9393  oicl  9498  oif  9499  wemapso2  9522  card2on  9523  en2lp  9582  ttrclselem1  9701  tctr  9714  r1tr  9755  rankdmr1  9780  r1pw  9824  r1pwALT  9825  rankuni  9842  scottex  9869  scottexOLD  9870  cardidm  9961  alephcard  10070  alephnbtwn  10071  cfub  10247  cardcf  10250  cflecard  10251  cfle  10252  cflim2  10262  cfidm  10274  isf32lem9  10360  itunisuc  10418  itunitc1  10419  itunitc  10420  ituniiun  10421  axcc2lem  10435  alephreg  10582  pwcfsdom  10583  cfpwsdom  10584  axunndlem1  10595  axpownd  10601  tskmcl  10841  addcompi  10894  addasspi  10895  mulcompi  10896  mulasspi  10897  distrpi  10898  addnidpi  10901  nlt1pi  10906  addcompq  10950  addcomnq  10951  mulcompq  10952  mulcomnq  10953  adderpq  10956  mulerpq  10957  addassnq  10958  mulassnq  10959  distrnq  10961  genpass  11009  addcompr  11021  mulcompr  11023  distrpr  11028  ltexprlem7  11042  addcomsr  11087  addasssr  11088  mulcomsr  11089  mulasssr  11090  distrsr  11091  indval0  12237  uzssz  12899  uzwo  12951  nn01to3  12981  xnn0xaddcl  13277  elixx3g  13401  iooid  13416  elfz2  13558  injresinjlem  13836  injresinj  13837  fleqceilz  13905  modifeq2int  13987  modfzo0difsn  13997  addmodlteq  14000  ltweuz  14015  fzofi  14028  fsuppmapnn0fiubex  14046  hashrabrsn  14426  hashrabsn01  14427  hashrabsn1  14428  elprchashprn2  14450  hashss  14463  hashsn01  14471  hash1snb  14474  hashgt12el  14477  hashgt12el2  14478  hashgt23el  14479  hashfzp1  14486  hashfundm  14497  hash2pwpr  14531  hashge2el2dif  14535  hash3tpde  14548  ffz0iswrd  14596  ccatsymb  14638  swrd00  14702  swrd0  14718  swrdwrdsymb  14722  pfx00  14734  pfx0  14735  repswswrd  14845  0csh0  14854  cshwcl  14859  cshwidxmod  14864  repswcshw  14873  cshw1  14883  s3sndisj  15028  s3iunsndisj  15029  xptrrel  15041  trclfvcotrg  15077  relexpfld  15110  reusq0  15540  modfsummods  15868  dvdsaddre2b  16387  gcdaddmlem  16604  prm23ge5  16897  pcmptcl  16973  prmgaplem5  17137  prmgaplem6  17138  cshwshash  17186  strle1  17240  strfvss  17269  strfvi  17272  setsnid  17290  ressbas  17318  ressbasssg  17319  ressbasssOLD  17322  resseqnbas  17324  ress0  17325  ressress  17329  0rest  17504  firest  17507  topnval  17509  xpsaddlem  17649  xpsvsca  17653  homffval  17768  comfffval  17776  oppchomfval  17792  oppcbas  17796  fullfunc  17987  fthfunc  17988  natfval  18028  fucbas  18042  fuchom  18043  arwval  18122  coafval  18143  xpcbas  18256  xpchomfval  18257  xpccofval  18260  oduval  18366  oduleval  18367  lubfun  18428  glbfun  18441  odujoin  18484  odumeet  18486  ipopos  18614  plusffval  18726  grpidval  18744  gsum0  18774  frmdplusg  18950  frmd0  18956  efmndbas  18967  efmndbasabf  18968  efmndplusg  18976  mgm2nsgrplem2  19018  mgm2nsgrplem3  19019  sgrp2rid2  19025  dfgrp2e  19074  grpinvfval  19089  grpinvfvalALT  19090  grpinvfvi  19093  grpsubfval  19094  grpsubfvalALT  19095  mulgfval  19179  mulgfvalALT  19180  mulgfvi  19183  cntrval  19433  oppgval  19461  oppgplusfval  19462  symgval  19485  snsymgefmndeq  19509  psgnfval  19614  odfval  19646  odfvalALT  19647  oppglsm  19756  efgval  19831  mgpval  20263  mgpplusg  20264  ringidval  20309  opprval  20466  opprmulfval  20467  dvdsrval  20489  invrfval  20517  dvrfval  20530  rrgval  20846  staffval  20994  scaffval  21051  rlmval  21362  rlmsca2  21370  2idlval  21440  nzerooringczr  21680  zrhval  21707  zlmlem  21716  zlmvsca  21721  chrval  21723  evpmss  21786  psgndiflemB  21800  ipffval  21848  thlbas  21896  thlle  21897  thloc  21899  pjfval  21906  dsmmval2  21936  asclfval  22078  psrplusg  22137  psrmulr  22142  psrvscafval  22148  mplval  22188  mplcoe3  22239  evlval  22301  psr1val  22396  vr1val  22402  ply1val  22404  ply1basfvi  22450  ply1plusgfvi  22451  psr1sca2  22460  ply1sca2  22463  ply1ascl  22469  cply1mul  22506  gsummoncoe1  22518  evl1fval  22538  evl1fval1  22541  mamufacex  22603  mavmulsolcl  22758  marrepfval  22767  marepvfval  22772  submafval  22786  mdetfval  22793  mdetfval1  22797  mdetunilem7  22825  mdetunilem8  22826  madufval  22844  minmar1fval  22853  mp2pm2mplem4  23016  toponsspwpw  23129  tgdif0  23199  indislem  23207  resstopn  23393  iocpnfordt  23422  icomnfordt  23423  hmeofval  23966  ussval  24467  nmfval  24796  nghmfval  24930  pcofval  25220  tcphval  25428  ioombl  25775  ibladdlem  26030  itgaddlem1  26033  iblabs  26039  dvbsss  26112  perfdvf  26113  mdegfval  26270  deg1fval  26288  deg1fvi  26293  uc1pval  26348  mon1pval  26350  2irrexpq  26947  lgsqrmodndvds  27568  gausslemma2dlem1a  27580  2lgs  27622  2sqreultblem  27663  2sqreunnltblem  27666  newval  28079  leftval  28093  rightval  28094  lltr  28106  oldssmade  28111  oldss  28114  lrold  28141  ttglem  29280  axcontlem12  29380  vtxval  29405  iedgval  29406  edgval  29454  usgr1v  29664  nbuhgr  29751  nbumgr  29755  uhgrnbgr0nb  29762  nbgr1vtx  29766  nbgrnself2  29768  nbusgrvtxm1  29787  sizusglecusg  29871  g0wlk0  30058  wlkreslem  30075  lfgrwlkprop  30097  wwlks  30251  wwlksn  30253  wspthsn  30264  iswwlksnon  30269  iswspthsnon  30272  0enwwlksnge1  30280  wwlksnfi  30322  clwwlk  30401  umgrclwwlkge2  30409  clwlkclwwlklem2a4  30415  clwwlkn  30444  clwwlknonmpo  30507  clwwlknon  30508  clwwlk0on0  30510  clwwlknon1le1  30519  1conngr  30616  eupth2lem3lem7  30656  frgr1v  30693  nfrgr2v  30694  1to2vfriswmgr  30701  2wspmdisj  30759  frgrreggt1  30815  frgrreg  30816  frgrregord013  30817  frgrogt3nreg  30819  friendship  30821  avril1  30885  vafval  31026  bafval  31027  smfval  31028  vsfval  31056  bcsiALT  31602  of0r  33095  fracval  33689  fracbas  33690  resvsca  33716  resvlem  33717  cntnevol  34683  signsw0glem  35005  bnj1189  35462  r1wf  35547  rankscottu  35580  noinfepregs  35603  kardval  35622  kard0b  35629  kardcard2b  35635  rankkardu  35641  fmlafvel  35914  gonan0  35921  satffun  35938  mvtval  36029  mexval  36031  mexval2  36032  mdvval  36033  mrsubfval  36037  mrsubrn  36042  msubfval  36053  elmsubrn  36057  msubrn  36058  mvhfval  36062  mpstval  36064  msrfval  36066  mstaval  36073  mppsval  36101  mthmval  36104  antnestlaw2  36221  dfrdg3  36323  fvsingle  36447  unisnif  36452  funpartfv  36474  fullfunfv  36476  linedegen  36672  axtcond  37046  csbttc  37077  mh-setindnd  37105  bj-ax6e  37347  axc11n11r  37365  bj-ax12v3ALT  37368  bj-sbsb  37529  bj-nfcsym  37591  bj-snex  37728  bj-restsnid  37786  bj-inftyexpitaudisj  37906  bj-inftyexpidisj  37911  finxpreclem4  38097  finxp00  38105  isinf2  38108  wl-nfs1t  38249  matunitlindflem1  38324  itg2addnclem  38379  ibladdnclem  38384  itgaddnclem1  38386  iblabsnc  38392  iblmulc2nc  38393  ftc1anclem8  38408  ismgmOLD  38559  tsbi1  38840  tsbi2  38841  ac6s6  38879  equid1  39731  ax12fromc15  39737  equid1ALT  39757  dvelimf-o  39761  ax12inda2ALT  39778  ax12inda2  39779  sn-axprlem3  43047  fsuppind  43380  mzpmfp  43536  itgocn  43949  mendbas  43965  mendplusgfval  43966  mendmulrfval  43968  mendsca  43970  mendvscafval  43971  arearect  44000  areaquad  44001  fpwfvss  44196  safesnsupfidom1o  44201  sn1dom  44310  or3or  44807  uneqsn  44809  addcomgi  45222  ax6e2ndeq  45326  2sb5ndVD  45676  2sb5ndALT  45698  sqwvfoura  47000  sqwvfourb  47001  fourierswlem  47002  fouriersw  47003  hspdifhsp  47388  hspmbllem2  47399  hspmbl  47401  et-ltneverrefl  47643  tz6.12-afv  47968  ndmaovcl  47998  tz6.12-afv2  48035  otiunsndisjX  48074  fvmptrab  48087  nltle2tri  48108  fzopredsuc  48119  iccpartiltu  48229  iccpartigtl  48230  iccpartlt  48231  icceuelpartlem  48242  iccpartnel  48245  elsprel  48282  sprssspr  48288  sprsymrelfvlem  48297  prprelprb  48324  prprspr2  48325  fmtnoprmfac1  48375  fmtnoprmfac2  48377  prmdvdsfmtnof1lem2  48395  prminf2  48398  lighneallem4  48420  requad1  48445  requad2  48446  evenprm2  48537  even3prm2  48542  fpprbasnn  48552  stgoldbwt  48599  pgnbgreunbgrlem2lem1  48937  pgnbgreunbgrlem2lem2  48938  pgnbgreunbgrlem2lem3  48939  upwlkbprop  48961  pgrpgt2nabl  49203  suppmptcfin  49213  linc1  49262  lindslinindsimp2lem5  49299  1aryenef  49482  2aryenef  49493  reorelicc  49547  rrxsphere  49585  fvconst0ci  49726  fvconstdomi  49727  upfval  50011  reldmprcof1  50216  reldmprcof2  50217  lmdfval  50484  cmdfval  50485  setrec2lem1  50528  setrec2mpt  50532