Theorem pm2.61i 175

Description: Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)

Hypotheses

Ref	Expression
pm2.61i.1	⊢ (𝜑 → 𝜓)
pm2.61i.2	⊢ (¬ 𝜑 → 𝜓)

Assertion

Ref	Expression
pm2.61i	⊢ 𝜓

Proof of Theorem pm2.61i

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		pm2.61i.2	. . 3 ⊢ (¬ 𝜑 → 𝜓)
3		pm2.61i.1	. . 3 ⊢ (𝜑 → 𝜓)
4	2, 3	ja 172	. 2 ⊢ ((𝜑 → 𝜑) → 𝜓)
5	1, 4	ax-mp 5	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  176  pm2.61nii  177  pm2.61iii  178  pm2.65i  184  pm5.21nii  367  pm5.18  370  biass  373  pm2.61ian  827  ecase3  979  4cases  987  pm4.42  995  ifpid  1019  elimh  1024  elimhOLD  1027  3ecase  1429  ax6e  2238  ax12  2292  exdistrf  2321  ax12OLD  2329  equvini  2334  dfsb2  2361  sbequi  2363  sbi1  2380  sbcom3  2399  sbco2  2403  sbco3  2405  sb9  2414  ax12vALT  2416  hbs1  2424  nfsb  2428  2ax6e  2438  sbal  2450  eujustALT  2461  pm2.61ine  2865  ralcom2  3083  eueq2  3347  moeq3  3350  mo2icl  3352  sbc2or  3411  sbcimdvOLD  3466  unineq  3836  csb0  3934  sbcel12  3935  sbcne12  3938  sbcel2  3941  csbidm  3954  csbun  3961  csbin  3962  ralidm  4027  ifsb  4049  ifid  4075  ifnot  4083  ifan  4084  ifor  4085  csbif  4088  elimhyp  4096  elimhyp2v  4097  elimhyp3v  4098  elimhyp4v  4099  elimdhyp  4101  keephyp2v  4103  keephyp3v  4104  eqoreldifOLD  4173  rabsnif  4202  tppreqb  4277  ssunsn2  4299  n0snor2el  4304  elpreqprlem  4333  dfopif  4337  csbuni  4402  sbcbr  4637  unisn2  4722  intabs  4752  class2set  4758  snexALT  4778  dtru  4783  dtruALT  4826  snex  4835  dtruALT2  4838  copsexg  4882  csbopab  4932  dfid3  4954  csbxp  5123  csbres  5320  csbima12  5402  soirri  5441  csbrn  5514  dmsnopss  5525  dmsnsnsn  5531  opswap  5540  unixpid  5587  nsuceq0  5722  ordsssuc2  5731  iotassuni  5784  iotaex  5785  dfiota4  5796  csbiota  5797  dffv3  6099  fvrn0  6126  ndmfv  6128  elfv2ex  6139  fveqres  6140  csbfv12  6141  csbfv  6143  dffv2  6181  fvco4i  6186  fvmptss  6201  fvmptex  6203  fvmptss2  6212  f0cli  6278  fvunsn  6350  fconst5  6376  csbriota  6523  riotassuni  6547  csbov123  6585  csbov  6586  0neqopab  6596  brfvopab  6598  elimdelov  6634  ovif12  6637  ndmovcl  6717  ndmovord  6722  elovmpt3imp  6788  difsnexi  6864  ordsuc  6906  ordsucelsuc  6914  1stval  7061  2ndval  7062  1st2val  7085  2nd2val  7086  el2mpt2csbcl  7137  bropopvvv  7142  bropfvvvvlem  7143  bropfvvvv  7144  suppimacnv  7193  suppssdm  7195  ressuppss  7201  suppun  7202  extmptsuppeq  7206  funsssuppss  7208  fczsupp0  7211  suppss  7212  suppssov1  7214  suppss2  7216  suppssfv  7218  supp0cosupp0  7221  imacosupp  7222  mpt2xopynvov0  7231  mpt2xopoveqd  7234  pwuninel  7288  smofvon2  7340  om0x  7486  brdomg  7851  snfi  7923  sdomirr  7982  domunsn  7995  2pwuninel  8000  snnen2o  8034  suppeqfsuppbi  8172  fsuppun  8177  funsnfsupp  8182  fipwuni  8215  oicl  8317  oif  8318  wemapso2  8341  card2on  8342  en2lp  8393  tctr  8499  r1tr  8522  rankdmr1  8547  r1pw  8591  r1pwALT  8592  rankuni  8609  scottex  8631  cardidm  8668  alephcard  8776  alephnbtwn  8777  cdacomen  8886  cfub  8954  cardcf  8957  cflecard  8958  cfle  8959  cflim2  8968  cfidm  8980  isf32lem9  9066  itunisuc  9124  itunitc1  9125  itunitc  9126  ituniiun  9127  axcc2lem  9141  alephreg  9283  pwcfsdom  9284  cfpwsdom  9285  axunndlem1  9296  axpownd  9302  tskmcl  9542  addcompi  9595  addasspi  9596  mulcompi  9597  mulasspi  9598  distrpi  9599  addnidpi  9602  nlt1pi  9607  addcompq  9651  addcomnq  9652  mulcompq  9653  mulcomnq  9654  adderpq  9657  mulerpq  9658  addassnq  9659  mulassnq  9660  distrnq  9662  genpass  9710  addcompr  9722  mulcompr  9724  distrpr  9729  ltexprlem7  9743  addcomsr  9787  addasssr  9788  mulcomsr  9789  mulasssr  9790  distrsr  9791  uzssz  11583  uzwo  11627  nn01to3  11657  xnn0xaddcl  11940  elixx3g  12059  iooid  12074  elfz2  12204  injresinjlem  12450  injresinj  12451  fleqceilz  12515  modifeq2int  12594  modfzo0difsn  12604  addmodlteq  12607  ltweuz  12622  fzofi  12635  fsuppmapnn0fiubex  12654  hashrabrsn  13022  hashrabsn01  13023  hashrabsn1  13024  elprchashprn2  13045  hashss  13058  hashsn01  13065  hash1snb  13068  hashgt12el  13070  hashgt12el2  13071  hashfzp1  13078  hash2pwpr  13115  hashge2el2dif  13117  ccatsymb  13219  swrd00  13270  swrd0  13286  swrdccatin1  13334  repswswrd  13382  0csh0  13390  cshwcl  13395  cshwidxmod  13400  repswcshw  13409  cshw1  13419  s3sndisj  13554  s3iunsndisj  13555  xptrrel  13567  trclfvcotrg  13605  relexpfld  13637  modfsummods  14366  pwm1geoser  14439  dvdsaddre2b  14867  zeneo  14901  gcdaddmlem  15083  prm23ge5  15358  pcmptcl  15433  prmgaplem5  15597  prmgaplem6  15598  cshwshash  15649  strfvss  15713  strfvi  15741  setsnid  15743  ressbas  15757  ressbasss  15759  resslem  15760  ress0  15761  ressress  15765  strle1  15800  0rest  15913  firest  15916  topnval  15918  xpsaddlem  16058  xpsvsca  16062  homffval  16173  comfffval  16181  oppchomfval  16197  oppcbas  16201  fullfunc  16389  fthfunc  16390  natfval  16429  fucbas  16443  fuchom  16444  arwval  16516  coafval  16537  xpcbas  16641  xpchomfval  16642  xpccofval  16645  lubfun  16803  glbfun  16816  oduval  16953  oduleval  16954  odumeet  16963  odujoin  16965  ipopos  16983  plusffval  17070  grpidval  17083  gsum0  17101  frmdplusg  17214  frmd0  17220  mgm2nsgrplem2  17229  mgm2nsgrplem3  17230  sgrp2rid2  17236  dfgrp2e  17271  grpinvfval  17283  grpinvfvi  17286  grpsubfval  17287  mulgfval  17365  mulgfvi  17368  cntrval  17575  oppgval  17600  oppgplusfval  17601  symgbas  17623  symgplusg  17632  psgnfval  17743  odfval  17775  oppglsm  17880  efgval  17953  mgpval  18315  mgpplusg  18316  ringidval  18326  opprval  18447  opprmulfval  18448  dvdsrval  18468  invrfval  18496  dvrfval  18507  staffval  18670  scaffval  18704  rlmval  19012  rlmsca2  19022  2idlval  19054  rrgval  19108  asclfval  19155  psrplusg  19202  psrmulr  19205  psrvscafval  19211  mplval  19249  mplcoe3  19287  evlval  19345  psr1val  19377  vr1val  19383  ply1val  19385  ply1basfvi  19432  ply1plusgfvi  19433  psr1sca2  19442  ply1sca2  19445  ply1ascl  19449  cply1mul  19485  gsummoncoe1  19495  evl1fval  19513  evl1fval1  19516  zrhval  19675  zlmlem  19684  zlmvsca  19689  chrval  19692  evpmss  19751  psgndiflemB  19765  ipffval  19812  thlbas  19859  thlle  19860  thloc  19862  pjfval  19869  dsmmval2  19899  mamufacex  20014  mavmulsolcl  20176  marrepfval  20185  marepvfval  20190  submafval  20204  mdetfval  20211  mdetfval1  20215  mdetunilem7  20243  mdetunilem8  20244  madufval  20262  minmar1fval  20271  mp2pm2mplem4  20433  tgdif0  20607  indislem  20614  resstopn  20800  iocpnfordt  20829  icomnfordt  20830  hmeofval  21371  ussval  21873  nmfval  22203  nghmfval  22336  pcofval  22618  tchval  22825  ioombl  23140  ibladdlem  23392  itgaddlem1  23395  iblabs  23401  dvbsss  23472  perfdvf  23473  mdegfval  23626  deg1fval  23644  deg1fvi  23649  uc1pval  23703  mon1pval  23705  lgsqrmodndvds  24878  gausslemma2dlem1a  24890  2lgs  24932  ttglem  25556  axcontlem12  25655  usgraedgprv  25905  usgra1v  25919  nbusgra  25957  nbgra0nb  25958  nbgranself2  25965  cusgra1v  25990  uvtxisvtx  26018  uvtx0  26019  uvtx01vtx  26020  1conngra  26203  wwlknfi  26266  wlk0  26289  clwwlkprop  26298  clwwlkgt0  26299  clwwlknprop  26300  clwlkisclwwlklem2a4  26312  2wlkonot3v  26402  2spthonot3v  26403  vdgrf  26425  nbhashuvtx1  26442  frgra2v  26526  1to2vfriswmgra  26533  2pthfrgra  26538  frgrancvvdeqlem2  26558  2spotdisj  26588  2spotiundisj  26589  2spotmdisj  26595  frgrareggt1  26643  frgrareg  26644  frgraregord013  26645  frgraogt3nreg  26647  friendship  26649  avril1  26711  vafval  26842  bafval  26843  smfval  26844  vsfval  26872  bcsiALT  27420  resvsca  29161  resvlem  29162  cntnevol  29618  signsw0glem  29956  bnj1189  30331  mvtval  30651  mexval  30653  mexval2  30654  mdvval  30655  mrsubfval  30659  mrsubrn  30664  msubfval  30675  elmsubrn  30679  msubrn  30680  mvhfval  30684  mpstval  30686  msrfval  30688  mstaval  30695  mppsval  30723  mthmval  30726  dfrdg3  30946  trpredlem1  30971  bdayelon  31079  fvsingle  31197  unisnif  31202  funpartfv  31222  fullfunfv  31224  linedegen  31420  bj-ax6e  31842  axc11n11r  31860  bj-ax12v3ALT  31863  bj-dtru  31985  bj-sbsb  32012  bj-nfcsym  32079  bj-restsnid  32221  bj-toponss  32241  bj-inftyexpidisj  32274  csbdif  32347  finxpreclem4  32407  finxp00  32415  wl-nfs1t  32503  wl-sbcom3  32551  matunitlindflem1  32575  itg2addnclem  32631  ibladdnclem  32636  itgaddnclem1  32638  iblabsnc  32644  iblmulc2nc  32645  ftc1anclem8  32662  ismgmOLD  32819  tsbi1  33110  tsbi2  33111  ac6s6  33150  equid1  33202  ax12fromc15  33208  equid1ALT  33228  dvelimf-o  33232  ax12inda2ALT  33249  ax12inda2  33250  mzpmfp  36328  itgocn  36753  mendbas  36773  mendplusgfval  36774  mendmulrfval  36776  mendsca  36778  mendvscafval  36779  arearect  36820  areaquad  36821  or3or  37339  uneqsn  37341  addcomgi  37681  ax6e2ndeq  37796  2sb5ndVD  38168  2sb5ndALT  38190  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  hspdifhsp  39506  hspmbllem2  39517  hspmbl  39519  tz6.12-afv  39902  ndmaovcl  39932  nltle2tri  39942  fzopredsuc  39946  iccpartiltu  39960  iccpartigtl  39961  iccpartlt  39962  icceuelpartlem  39973  iccpartnel  39976  fmtnoprmfac1  40015  fmtnoprmfac2  40017  prmdvdsfmtnof1lem2  40035  prminf2  40038  lighneallem4  40065  evenprm2  40161  stgoldbwt  40198  pfx00  40247  pfx0  40248  otiunsndisjX  40317  usgr1v  40482  nbuhgr  40565  nbumgr  40569  uhgrnbgr0nb  40576  nbgr1vtx  40580  nbgrnself2  40585  nbusgrvtxm1  40607  uvtxa0  40620  sizusglecusg  40679  wlkbProp  40817  g01wlk0  40860  1wlkreslem  40878  lfgrwlkprop  40896  wwlks  41038  wwlksn  41040  wspthsn  41046  iswwlksnon  41051  iswspthsnon  41052  0enwwlksnge1  41060  wwlksnfi  41112  wwlksnonfi  41127  wspn0  41131  wwlks2onv  41158  2wspdisj  41165  2wspiundisj  41166  clwwlks  41187  clwwlksn  41189  clwlkclwwlklem2a4  41206  umgrclwwlksge2  41219  clwwlksnfi  41220  1conngr  41361  eupth2lem3lem7  41402  frgr1v  41441  nfrgr2v  41442  1to2vfriswmgr  41449  frgrncvvdeqlem2  41470  2wspmdisj  41501  av-frgrareggt1  41547  av-frgrareg  41548  av-frgraregord013  41549  av-frgraogt3nreg  41551  av-friendship  41553  nzerooringczr  41864  pgrpgt2nabl  41941  suppmptcfin  41954  linc1  42008  lindslinindsimp2lem5  42045  setrec2lem1  42239