Theorem pm2.61i 183

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  184  pm2.61nii  185  pm2.61iii  186  pm2.65iOLD  196  pm5.21nii  380  pm5.18  383  biass  387  pm2.61ian  821  ecase3  1044  4cases  1052  pm4.42  1065  ifpid  1088  elimh  1094  3ecase  1495  norass  1557  ax6e  2414  ax12  2454  exdistrf  2478  equvini  2486  ax12vALT  2500  2ax6e  2502  sb1  2509  sb2  2510  sb4a  2511  dfsb1  2512  dfsb2  2524  sbcom3  2537  sbco2  2542  sbco3  2544  sb9  2550  eujustALT  2599  pm2.61ine  3040  ralcom2  3364  eueq2  3673  moeq3  3675  mo2icl  3677  sbc2or  3753  unineq  4240  csb0  4364  sbcel12  4365  sbcne12  4369  sbcel2  4372  csbidm  4387  csbun  4395  csbin  4396  csbdif  4479  ifsb  4494  ifid  4521  ifnot  4533  ifan  4534  ifor  4535  csbif  4538  elimhyp  4546  elimhyp2v  4547  elimhyp3v  4548  elimhyp4v  4549  elimdhyp  4551  keephyp2v  4553  keephyp3v  4554  rmosn  4678  rabsnif  4682  tppreqb  4765  ssunsn2  4785  n0snor2el  4791  preq12nebg  4821  opthprneg  4823  elpreqprlem  4824  dfopif  4828  csbuni  4896  disjord  5089  sbcbr  5155  unisn2  5262  intabs  5305  class2set  5311  dtruALT2  5327  snexALT  5340  dtruALT  5345  axprlem3  5382  axprlem3OLD  5386  axprglem  5393  axprg  5394  snexOLD  5399  exneq  5403  copsexgwOLD  5459  copsexg  5460  snopeqop  5475  csbopab  5526  dfid3  5545  csbxp  5748  csbcnv  5858  csbres  5968  csbima12  6068  soirri  6113  csbrn  6190  dmsnopss  6201  dmsnsnsn  6207  opswap  6216  unixpid  6271  predres  6326  nsuceq0  6431  ordsssuc2  6439  iotassuni  6496  iotaex  6497  csbiota  6514  dffv3  6863  fvrn0  6895  ndmfv  6899  elfv2ex  6910  fveqres  6911  csbfv12  6912  csbfv  6914  dffv2  6962  fvco4i  6969  fvmptss  6988  fvmptex  6990  fvmptss2  7002  fvmptrabfv  7008  f0cli  7079  fvunsn  7163  fconst5  7190  csbriota  7368  riotassuni  7393  oprabidw  7427  csbov123  7440  csbov  7441  fvmptopab  7451  brfvopab  7453  elimdelov  7492  ovif12  7496  ifmpt2v  7498  ndmovcl  7581  ndmovord  7586  elovmpt3imp  7653  difsnexi  7744  ordsuc  7794  ordsucelsuc  7802  1stval  7972  2ndval  7973  1st2val  7998  2nd2val  7999  el2mpocsbcl  8064  bropopvvv  8069  bropfvvvvlem  8070  bropfvvvv  8071  suppimacnv  8154  suppssdm  8157  ressuppss  8163  suppun  8164  extmptsuppeq  8168  funsssuppss  8170  fczsupp0  8173  suppss  8174  suppss2  8180  suppssfv  8182  suppco  8186  mpoxopynvov0  8198  mpoxopoveqd  8201  pwuninelOLD  8256  smofvon2  8327  om0x  8488  mapssfset  8832  brdomg  8939  snfi  9024  sdomirr  9086  domunsn  9099  2pwuninel  9104  unfi  9139  cnvfi  9144  suppeqfsuppbi  9325  fsuppun  9333  funsnfsupp  9338  fipwuni  9372  oicl  9477  oif  9478  wemapso2  9501  card2on  9502  en2lp  9561  ttrclselem1  9680  tctr  9693  r1tr  9734  rankdmr1  9759  r1pw  9803  r1pwALT  9804  rankuni  9821  scottex  9843  cardidm  9917  alephcard  10026  alephnbtwn  10027  cfub  10205  cardcf  10208  cflecard  10209  cfle  10210  cflim2  10220  cfidm  10232  isf32lem9  10318  itunisuc  10376  itunitc1  10377  itunitc  10378  ituniiun  10379  axcc2lem  10393  alephreg  10540  pwcfsdom  10541  cfpwsdom  10542  axunndlem1  10553  axpownd  10559  tskmcl  10799  addcompi  10852  addasspi  10853  mulcompi  10854  mulasspi  10855  distrpi  10856  addnidpi  10859  nlt1pi  10864  addcompq  10908  addcomnq  10909  mulcompq  10910  mulcomnq  10911  adderpq  10914  mulerpq  10915  addassnq  10916  mulassnq  10917  distrnq  10919  genpass  10967  addcompr  10979  mulcompr  10981  distrpr  10986  ltexprlem7  11000  addcomsr  11045  addasssr  11046  mulcomsr  11047  mulasssr  11048  distrsr  11049  indval0  12199  uzssz  12860  uzwo  12912  nn01to3  12942  xnn0xaddcl  13238  elixx3g  13362  iooid  13377  elfz2  13519  injresinjlem  13796  injresinj  13797  fleqceilz  13864  modifeq2int  13946  modfzo0difsn  13956  addmodlteq  13959  ltweuz  13974  fzofi  13987  fsuppmapnn0fiubex  14005  hashrabrsn  14385  hashrabsn01  14386  hashrabsn1  14387  elprchashprn2  14409  hashss  14422  hashsn01  14429  hash1snb  14432  hashgt12el  14435  hashgt12el2  14436  hashgt23el  14437  hashfzp1  14444  hashfundm  14455  hash2pwpr  14489  hashge2el2dif  14493  hash3tpde  14506  ffz0iswrd  14554  ccatsymb  14596  swrd00  14658  swrd0  14672  swrdwrdsymb  14676  pfx00  14688  pfx0  14689  repswswrd  14797  0csh0  14806  cshwcl  14811  cshwidxmod  14816  repswcshw  14825  cshw1  14835  s3sndisj  14980  s3iunsndisj  14981  xptrrel  14993  trclfvcotrg  15029  relexpfld  15062  reusq0  15492  modfsummods  15821  dvdsaddre2b  16341  gcdaddmlem  16558  prm23ge5  16851  pcmptcl  16927  prmgaplem5  17091  prmgaplem6  17092  cshwshash  17140  strle1  17194  strfvss  17223  strfvi  17226  setsnid  17244  ressbas  17272  ressbasssg  17273  ressbasssOLD  17276  resseqnbas  17278  ress0  17279  ressress  17283  0rest  17458  firest  17461  topnval  17463  xpsaddlem  17603  xpsvsca  17607  homffval  17722  comfffval  17730  oppchomfval  17746  oppcbas  17750  fullfunc  17941  fthfunc  17942  natfval  17982  fucbas  17996  fuchom  17997  arwval  18076  coafval  18097  xpcbas  18210  xpchomfval  18211  xpccofval  18214  oduval  18320  oduleval  18321  lubfun  18382  glbfun  18395  odujoin  18438  odumeet  18440  ipopos  18568  plusffval  18680  grpidval  18695  gsum0  18718  frmdplusg  18888  frmd0  18894  efmndbas  18905  efmndbasabf  18906  efmndplusg  18914  mgm2nsgrplem2  18956  mgm2nsgrplem3  18957  sgrp2rid2  18963  dfgrp2e  19005  grpinvfval  19020  grpinvfvalALT  19021  grpinvfvi  19024  grpsubfval  19025  grpsubfvalALT  19026  mulgfval  19111  mulgfvalALT  19112  mulgfvi  19115  cntrval  19359  oppgval  19387  oppgplusfval  19388  symgval  19411  snsymgefmndeq  19435  psgnfval  19540  odfval  19572  odfvalALT  19573  oppglsm  19682  efgval  19757  mgpval  20189  mgpplusg  20190  ringidval  20229  opprval  20383  opprmulfval  20384  dvdsrval  20406  invrfval  20434  dvrfval  20447  rrgval  20743  staffval  20887  scaffval  20944  rlmval  21255  rlmsca2  21263  2idlval  21318  nzerooringczr  21529  zrhval  21556  zlmlem  21565  zlmvsca  21570  chrval  21572  evpmss  21635  psgndiflemB  21649  ipffval  21697  thlbas  21745  thlle  21746  thloc  21748  pjfval  21755  dsmmval2  21785  asclfval  21927  psrplusg  21986  psrmulr  21991  psrvscafval  21997  mplval  22037  mplcoe3  22088  evlval  22150  psr1val  22245  vr1val  22251  ply1val  22253  ply1basfvi  22299  ply1plusgfvi  22300  psr1sca2  22309  ply1sca2  22312  ply1ascl  22318  cply1mul  22356  gsummoncoe1  22368  evl1fval  22388  evl1fval1  22391  mamufacex  22453  mavmulsolcl  22608  marrepfval  22617  marepvfval  22622  submafval  22636  mdetfval  22643  mdetfval1  22647  mdetunilem7  22675  mdetunilem8  22676  madufval  22694  minmar1fval  22703  mp2pm2mplem4  22866  toponsspwpw  22979  tgdif0  23049  indislem  23057  resstopn  23243  iocpnfordt  23272  icomnfordt  23273  hmeofval  23815  ussval  24316  nmfval  24645  nghmfval  24779  pcofval  25069  tcphval  25277  ioombl  25624  ibladdlem  25879  itgaddlem1  25882  iblabs  25888  dvbsss  25961  perfdvf  25962  mdegfval  26119  deg1fval  26137  deg1fvi  26142  uc1pval  26197  mon1pval  26199  2irrexpq  26793  lgsqrmodndvds  27414  gausslemma2dlem1a  27426  2lgs  27468  2sqreultblem  27509  2sqreunnltblem  27512  newval  27925  leftval  27939  rightval  27940  lltr  27952  oldssmade  27957  oldss  27960  lrold  27987  ttglem  29073  axcontlem12  29173  vtxval  29198  iedgval  29199  edgval  29247  usgr1v  29454  nbuhgr  29541  nbumgr  29545  uhgrnbgr0nb  29552  nbgr1vtx  29556  nbgrnself2  29558  nbusgrvtxm1  29577  sizusglecusg  29661  g0wlk0  29848  wlkreslem  29865  lfgrwlkprop  29883  wwlks  30032  wwlksn  30034  wspthsn  30045  iswwlksnon  30050  iswspthsnon  30053  0enwwlksnge1  30061  wwlksnfi  30103  clwwlk  30182  umgrclwwlkge2  30190  clwlkclwwlklem2a4  30196  clwwlkn  30225  clwwlknonmpo  30288  clwwlknon  30289  clwwlk0on0  30291  clwwlknon1le1  30300  1conngr  30393  eupth2lem3lem7  30433  frgr1v  30470  nfrgr2v  30471  1to2vfriswmgr  30478  2wspmdisj  30536  frgrreggt1  30592  frgrreg  30593  frgrregord013  30594  frgrogt3nreg  30596  friendship  30598  avril1  30662  vafval  30803  bafval  30804  smfval  30805  vsfval  30833  bcsiALT  31379  of0r  32878  fracval  33488  fracbas  33489  resvsca  33515  resvlem  33516  cntnevol  34522  signsw0glem  34844  bnj1189  35301  r1wf  35389  noinfepregs  35426  fmlafvel  35732  gonan0  35739  satffun  35756  mvtval  35847  mexval  35849  mexval2  35850  mdvval  35851  mrsubfval  35855  mrsubrn  35860  msubfval  35871  elmsubrn  35875  msubrn  35876  mvhfval  35880  mpstval  35882  msrfval  35884  mstaval  35891  mppsval  35919  mthmval  35922  antnestlaw2  36039  dfrdg3  36141  fvsingle  36265  unisnif  36270  funpartfv  36292  fullfunfv  36294  linedegen  36490  axtcond  36835  csbttc  36866  mh-setindnd  36894  bj-ax6e  37137  axc11n11r  37155  bj-ax12v3ALT  37158  bj-sbsb  37319  bj-nfcsym  37381  bj-snex  37517  bj-restsnid  37574  bj-inftyexpitaudisj  37694  bj-inftyexpidisj  37699  finxpreclem4  37885  finxp00  37893  isinf2  37896  wl-nfs1t  38037  matunitlindflem1  38112  itg2addnclem  38167  ibladdnclem  38172  itgaddnclem1  38174  iblabsnc  38180  iblmulc2nc  38181  ftc1anclem8  38196  ismgmOLD  38346  tsbi1  38629  tsbi2  38630  ac6s6  38668  equid1  39520  ax12fromc15  39526  equid1ALT  39546  dvelimf-o  39550  ax12inda2ALT  39567  ax12inda2  39568  sn-axprlem3  42834  fsuppind  43169  mzpmfp  43325  itgocn  43738  mendbas  43754  mendplusgfval  43755  mendmulrfval  43757  mendsca  43759  mendvscafval  43760  arearect  43789  areaquad  43790  fpwfvss  43985  safesnsupfidom1o  43990  sn1dom  44099  or3or  44596  uneqsn  44598  addcomgi  45028  ax6e2ndeq  45132  2sb5ndVD  45482  2sb5ndALT  45504  sqwvfoura  46799  sqwvfourb  46800  fourierswlem  46801  fouriersw  46802  hspdifhsp  47187  hspmbllem2  47198  hspmbl  47200  et-ltneverrefl  47442  tz6.12-afv  47764  ndmaovcl  47794  tz6.12-afv2  47831  otiunsndisjX  47870  fvmptrab  47883  nltle2tri  47904  fzopredsuc  47915  iccpartiltu  48025  iccpartigtl  48026  iccpartlt  48027  icceuelpartlem  48038  iccpartnel  48041  elsprel  48078  sprssspr  48084  sprsymrelfvlem  48093  prprelprb  48120  prprspr2  48121  fmtnoprmfac1  48171  fmtnoprmfac2  48173  prmdvdsfmtnof1lem2  48191  prminf2  48194  lighneallem4  48216  requad1  48241  requad2  48242  evenprm2  48333  even3prm2  48338  fpprbasnn  48348  stgoldbwt  48395  pgnbgreunbgrlem2lem1  48733  pgnbgreunbgrlem2lem2  48734  pgnbgreunbgrlem2lem3  48735  upwlkbprop  48757  pgrpgt2nabl  48985  suppmptcfin  48995  linc1  49044  lindslinindsimp2lem5  49081  1aryenef  49264  2aryenef  49275  reorelicc  49329  rrxsphere  49367  fvconst0ci  49509  fvconstdomi  49510  upfval  49794  reldmprcof1  49999  reldmprcof2  50000  lmdfval  50267  cmdfval  50268  setrec2lem1  50311  setrec2mpt  50315