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 161	. 2 ⊢ (¬ 𝜓 → 𝜓)
4	3	pm2.18i 131	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.65i  195  pm5.21nii  380  pm5.18  383  biass  386  pm2.61ian  808  ecase3  1025  4cases  1033  pm4.42  1046  ifpid  1068  elimh  1073  elimhOLD  1074  3ecase  1466  ax6e  2356  ax12  2402  exdistrf  2426  equvini  2434  equviniOLD  2435  ax12vALT  2449  2ax6e  2451  2ax6eOLD  2452  sb2  2458  sb1  2461  sb4a  2463  dfsb1  2464  dfsb2  2486  sbequiOLD  2488  sbi1OLD  2496  sbcom3  2502  sbco2  2507  sbco3  2509  sb9  2515  nfsb  2518  sbalOLD  2529  dfsb2ALT  2545  sbequiALT  2550  sbi1ALT  2560  sbco2ALT  2569  eujustALT  2615  pm2.61ine  3068  ralcom2  3324  eueq2  3637  moeq3  3639  mo2icl  3641  sbc2or  3715  unineq  4174  csb0  4279  sbcel12  4280  sbcne12  4284  sbcel2  4287  csbidm  4297  csbun  4305  csbin  4306  ralidm  4369  ifsb  4394  ifid  4420  ifnot  4431  ifan  4432  ifor  4433  csbif  4436  elimhyp  4444  elimhyp2v  4445  elimhyp3v  4446  elimhyp4v  4447  elimdhyp  4449  keephyp2v  4451  keephyp3v  4452  rmosn  4562  rabsnif  4566  tppreqb  4645  ssunsn2  4667  n0snor2el  4671  preq12nebg  4700  opthprneg  4702  elpreqprlem  4703  dfopif  4707  csbuni  4773  disjord  4951  sbcbr  5017  unisn2  5107  intabs  5136  class2set  5145  dtru  5162  snexALT  5174  dtruALT  5179  axprlem3  5217  snex  5223  dtruALT2  5227  copsexg  5273  snopeqop  5287  csbopab  5330  0nelopab  5340  dfid3  5349  csbxp  5536  csbres  5737  csbima12  5823  soirri  5862  csbrn  5935  dmsnopss  5946  dmsnsnsn  5952  opswap  5961  unixpid  6010  nsuceq0  6146  ordsssuc2  6154  iotassuni  6205  iotaex  6206  csbiota  6218  dffv3  6534  fvrn0  6566  ndmfv  6568  elfv2ex  6579  fveqres  6580  csbfv12  6581  csbfv  6583  dffv2  6623  fvco4i  6629  fvmptss  6646  fvmptex  6648  fvmptss2  6659  fvmptrabfv  6664  f0cli  6727  fvunsn  6804  fconst5  6835  csbriota  6989  riotassuni  7014  csbov123  7057  csbov  7058  fvmptopab  7068  brfvopab  7070  elimdelov  7106  ovif12  7109  ndmovcl  7189  ndmovord  7194  elovmpt3imp  7260  difsnexi  7340  ordsuc  7385  ordsucelsuc  7393  1stval  7547  2ndval  7548  1st2val  7573  2nd2val  7574  el2mpocsbcl  7636  bropopvvv  7641  bropfvvvvlem  7642  bropfvvvv  7643  suppimacnv  7692  suppssdm  7694  ressuppss  7700  suppun  7701  extmptsuppeq  7705  funsssuppss  7707  fczsupp0  7710  suppss  7711  suppssov1  7713  suppss2  7715  suppssfv  7717  suppco  7721  supp0cosupp0OLD  7724  imacosuppOLD  7726  mpoxopynvov0  7735  mpoxopoveqd  7738  pwuninel  7792  smofvon2  7845  om0x  7995  brdomg  8367  snfi  8442  sdomirr  8501  domunsn  8514  2pwuninel  8519  snnen2o  8553  suppeqfsuppbi  8693  fsuppun  8698  funsnfsupp  8703  fipwuni  8736  oicl  8839  oif  8840  wemapso2  8863  card2on  8864  en2lp  8915  tctr  9028  r1tr  9051  rankdmr1  9076  r1pw  9120  r1pwALT  9121  rankuni  9138  scottex  9160  cardidm  9234  alephcard  9342  alephnbtwn  9343  cfub  9517  cardcf  9520  cflecard  9521  cfle  9522  cflim2  9531  cfidm  9543  isf32lem9  9629  itunisuc  9687  itunitc1  9688  itunitc  9689  ituniiun  9690  axcc2lem  9704  alephreg  9850  pwcfsdom  9851  cfpwsdom  9852  axunndlem1  9863  axpownd  9869  tskmcl  10109  addcompi  10162  addasspi  10163  mulcompi  10164  mulasspi  10165  distrpi  10166  addnidpi  10169  nlt1pi  10174  addcompq  10218  addcomnq  10219  mulcompq  10220  mulcomnq  10221  adderpq  10224  mulerpq  10225  addassnq  10226  mulassnq  10227  distrnq  10229  genpass  10277  addcompr  10289  mulcompr  10291  distrpr  10296  ltexprlem7  10310  addcomsr  10355  addasssr  10356  mulcomsr  10357  mulasssr  10358  distrsr  10359  uzssz  12113  uzwo  12160  nn01to3  12190  xnn0xaddcl  12478  elixx3g  12601  iooid  12616  elfz2  12749  injresinjlem  13007  injresinj  13008  fleqceilz  13072  modifeq2int  13151  modfzo0difsn  13161  addmodlteq  13164  ltweuz  13179  fzofi  13192  fsuppmapnn0fiubex  13210  hashrabrsn  13581  hashrabsn01  13582  hashrabsn1  13583  elprchashprn2  13605  hashss  13618  hashsn01  13625  hash1snb  13628  hashgt12el  13631  hashgt12el2  13632  hashgt23el  13633  hashfzp1  13640  hash2pwpr  13680  hashge2el2dif  13684  ffz0iswrd  13737  ccatsymb  13780  swrd00  13842  swrd0  13856  swrdwrdsymb  13860  pfx00  13872  pfx0  13873  swrdccatin1  13923  repswswrd  13982  0csh0  13991  cshwcl  13996  cshwidxmod  14001  repswcshw  14010  cshw1  14020  s3sndisj  14161  s3iunsndisj  14162  xptrrel  14174  trclfvcotrg  14210  relexpfld  14242  reusq0  14656  modfsummods  14981  pwm1geoserOLD  15058  dvdsaddre2b  15490  gcdaddmlem  15705  prm23ge5  15981  pcmptcl  16056  prmgaplem5  16220  prmgaplem6  16221  cshwshash  16267  strfvss  16335  strfvi  16366  setsnid  16368  ressbas  16383  ressbasss  16385  resslem  16386  ress0  16387  ressress  16391  strle1  16421  0rest  16532  firest  16535  topnval  16537  xpsaddlem  16675  xpsvsca  16679  homffval  16789  comfffval  16797  oppchomfval  16813  oppcbas  16817  fullfunc  17005  fthfunc  17006  natfval  17045  fucbas  17059  fuchom  17060  arwval  17132  coafval  17153  xpcbas  17257  xpchomfval  17258  xpccofval  17261  lubfun  17419  glbfun  17432  oduval  17569  oduleval  17570  odumeet  17579  odujoin  17581  ipopos  17599  plusffval  17686  grpidval  17699  gsum0  17717  frmdplusg  17830  frmd0  17836  mgm2nsgrplem2  17845  mgm2nsgrplem3  17846  sgrp2rid2  17852  dfgrp2e  17887  grpinvfval  17899  grpinvfvalALT  17900  grpinvfvi  17903  grpsubfval  17904  grpsubfvalALT  17905  mulgfval  17983  mulgfvalALT  17984  mulgfvi  17987  cntrval  18190  oppgval  18216  oppgplusfval  18217  symgbas  18239  symgplusg  18248  psgnfval  18359  odfval  18391  odfvalALT  18392  oppglsm  18497  efgval  18570  mgpval  18932  mgpplusg  18933  ringidval  18943  opprval  19064  opprmulfval  19065  dvdsrval  19085  invrfval  19113  dvrfval  19124  staffval  19308  scaffval  19342  rlmval  19653  rlmsca2  19663  2idlval  19695  rrgval  19749  asclfval  19796  psrplusg  19849  psrmulr  19852  psrvscafval  19858  mplval  19896  mplcoe3  19934  evlval  19991  psr1val  20037  vr1val  20043  ply1val  20045  ply1basfvi  20092  ply1plusgfvi  20093  psr1sca2  20102  ply1sca2  20105  ply1ascl  20109  cply1mul  20145  gsummoncoe1  20155  evl1fval  20173  evl1fval1  20176  zrhval  20337  zlmlem  20346  zlmvsca  20351  chrval  20354  evpmss  20412  psgndiflemB  20426  ipffval  20474  thlbas  20522  thlle  20523  thloc  20525  pjfval  20532  dsmmval2  20562  mamufacex  20682  mavmulsolcl  20844  marrepfval  20853  marepvfval  20858  submafval  20872  mdetfval  20879  mdetfval1  20883  mdetunilem7  20911  mdetunilem8  20912  madufval  20930  minmar1fval  20939  mp2pm2mplem4  21101  toponsspwpw  21214  tgdif0  21284  indislem  21292  resstopn  21478  iocpnfordt  21507  icomnfordt  21508  hmeofval  22050  ussval  22551  nmfval  22881  nghmfval  23014  pcofval  23297  tcphval  23504  ioombl  23849  ibladdlem  24103  itgaddlem1  24106  iblabs  24112  dvbsss  24183  perfdvf  24184  mdegfval  24339  deg1fval  24357  deg1fvi  24362  uc1pval  24416  mon1pval  24418  2irrexpq  24994  lgsqrmodndvds  25611  gausslemma2dlem1a  25623  2lgs  25665  2sqreultblem  25706  2sqreunnltblem  25709  ttglem  26345  axcontlem12  26444  vtxval  26468  iedgval  26469  edgval  26517  usgr1v  26721  nbuhgr  26808  nbumgr  26812  uhgrnbgr0nb  26819  nbgr1vtx  26823  nbgrnself2  26825  nbusgrvtxm1  26844  sizusglecusg  26928  g0wlk0  27116  wlkreslem  27134  wlkreslemOLD  27136  lfgrwlkprop  27154  wwlks  27300  wwlksn  27302  wspthsn  27313  iswwlksnon  27318  iswspthsnon  27321  0enwwlksnge1  27329  wwlksnfi  27371  wwlksnfiOLD  27372  clwwlk  27448  umgrclwwlkge2  27456  clwlkclwwlklem2a4  27462  clwwlkn  27491  clwwlknfiOLD  27511  clwwlknonmpo  27555  clwwlknon  27556  clwwlk0on0  27558  clwwlknon1le1  27567  1conngr  27660  eupth2lem3lem7  27701  frgr1v  27742  nfrgr2v  27743  1to2vfriswmgr  27750  2wspmdisj  27808  frgrreggt1  27864  frgrreg  27865  frgrregord013  27866  frgrogt3nreg  27868  friendship  27870  avril1  27933  vafval  28071  bafval  28072  smfval  28073  vsfval  28101  bcsiALT  28647  resvsca  30557  resvlem  30558  cntnevol  31104  signsw0glem  31440  bnj1189  31895  hashfundm  31968  fmlafvel  32240  gonan0  32247  satffun  32264  mvtval  32355  mexval  32357  mexval2  32358  mdvval  32359  mrsubfval  32363  mrsubrn  32368  msubfval  32379  elmsubrn  32383  msubrn  32384  mvhfval  32388  mpstval  32390  msrfval  32392  mstaval  32399  mppsval  32427  mthmval  32430  dfrdg3  32650  trpredlem1  32675  fvsingle  32990  unisnif  32995  funpartfv  33015  fullfunfv  33017  linedegen  33213  bj-ax6e  33600  axc11n11r  33616  bj-ax12v3ALT  33619  bj-dtru  33704  bj-sbsb  33730  bj-nfcsym  33786  bj-restsnid  33977  bj-inftyexpitaudisj  34045  bj-inftyexpidisj  34050  csbdif  34137  finxpreclem4  34206  finxp00  34214  isinf2  34217  wl-nfs1t  34309  matunitlindflem1  34419  itg2addnclem  34474  ibladdnclem  34479  itgaddnclem1  34481  iblabsnc  34487  iblmulc2nc  34488  ftc1anclem8  34505  ismgmOLD  34660  tsbi1  34943  tsbi2  34944  ac6s6  34982  equid1  35566  ax12fromc15  35572  equid1ALT  35592  dvelimf-o  35596  ax12inda2ALT  35613  ax12inda2  35614  sn-axprlem3  38639  sn-dtru  38641  mzpmfp  38829  itgocn  39249  mendbas  39269  mendplusgfval  39270  mendmulrfval  39272  mendsca  39274  mendvscafval  39275  arearect  39307  areaquad  39308  sn1dom  39377  or3or  39856  uneqsn  39858  addcomgi  40327  ax6e2ndeq  40432  2sb5ndVD  40783  2sb5ndALT  40805  sqwvfoura  42055  sqwvfourb  42056  fourierswlem  42057  fouriersw  42058  hspdifhsp  42440  hspmbllem2  42451  hspmbl  42453  tz6.12-afv  42888  ndmaovcl  42918  tz6.12-afv2  42955  otiunsndisjX  42994  fvmptrab  43007  nltle2tri  43029  fzopredsuc  43039  iccpartiltu  43064  iccpartigtl  43065  iccpartlt  43066  icceuelpartlem  43077  iccpartnel  43080  elsprel  43119  sprssspr  43125  sprsymrelfvlem  43134  prprelprb  43161  prprspr2  43162  fmtnoprmfac1  43209  fmtnoprmfac2  43211  prmdvdsfmtnof1lem2  43229  prminf2  43232  lighneallem4  43257  requad1  43269  requad2  43270  evenprm2  43361  even3prm2  43366  fpprbasnn  43376  stgoldbwt  43423  upwlkbprop  43495  nzerooringczr  43821  pgrpgt2nabl  43894  suppmptcfin  43907  linc1  43960  lindslinindsimp2lem5  43997  reorelicc  44178  rrxsphere  44216  setrec2lem1  44276