Theorem pm2.61i 164

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	|- ( ph -> ps )
pm2.61i.2	|- ( -. ph -> ps )

Assertion

Ref	Expression
pm2.61i	|- ps

Proof of Theorem pm2.61i

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ph -> ph )
2		pm2.61i.2	. . 3 |- ( -. ph -> ps )
3		pm2.61i.1	. . 3 |- ( ph -> ps )
4	2, 3	ja 161	. 2 |- ( ( ph -> ph ) -> ps )
5	1, 4	ax-mp 5	1 |- ps

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  165  pm2.61nii  166  pm2.61iii  167  pm2.65i  173  pm5.21nii  353  pm5.18  356  biass  359  pm2.61ian  788  ecase3  939  4cases  947  elimh  954  pm4.42  958  3ecase  1333  ax6e  1971  exdistrf  2048  equvini  2060  dfsb2  2087  sbequi  2089  sbnOLD  2106  sbi1  2107  sbcom3  2128  sbco2  2134  sbco2OLD  2135  sbco3  2137  sbco3OLD  2138  sb9  2149  sb9iOLD  2151  ax12vALT  2153  hbs1  2163  nfsb  2168  2ax6e  2180  sbal1OLD  2194  sbal  2196  sbalOLD  2197  ax12  2227  equid1  2230  equid1ALT  2248  dvelimf-o  2252  ax12inda2ALT  2269  ax12inda2  2270  eujustALT  2278  moexexOLD  2372  pm2.61ine  2780  pm2.61neOLD  2783  rgen2aOLD  2892  ralcom2  3026  eueq2  3277  moeq3  3280  mo2icl  3282  sbc2or  3340  sbcimdv  3400  unineq  3748  csb0  3822  sbcel12  3823  sbcne12  3827  sbcel2  3831  csbidm  3846  csbun  3857  csbin  3860  ralidm  3931  ifsb  3952  ifid  3976  ifnot  3984  ifan  3985  ifor  3986  csbif  3989  elimhyp  3998  elimhyp2v  3999  elimhyp3v  4000  elimhyp4v  4001  elimdhyp  4003  keephyp2v  4005  keephyp3v  4006  rabsnif  4096  tppreqb  4168  ssunsn2  4186  dfopif  4210  csbuni  4273  sbcbr123  4498  sbcbr  4500  unisn2  4583  intabs  4608  class2set  4614  snexALT  4633  dtru  4638  dtruALT  4679  snex  4688  dtruALT2  4691  copsexg  4732  copsexgOLD  4733  otsndisj  4752  otiunsndisj  4753  csbopab  4779  dfid3  4796  nsuceq0  4958  ordsssuc2  4966  csbxp  5081  csbres  5276  csbima12  5354  soirri  5393  soirriOLD  5398  csbrn  5468  dmsnopss  5480  dmsnsnsn  5486  opswap  5495  unixpid  5542  iotassuni  5567  iotaex  5568  dfiota4  5579  csbiota  5580  dffv3  5862  fvrn0  5888  ndmfv  5890  fveqres  5900  csbfv12  5901  csbfv  5904  dffv2  5940  fvco4i  5945  fvmptss  5958  fvmptex  5960  fvmptss2  5969  f0cli  6032  fvunsn  6093  fconst5  6118  csbriota  6257  riotassuniOLD  6282  csbov123  6315  csbov  6316  0neqopab  6325  elimdelov  6362  ovif12  6365  ndmovcl  6444  ndmovord  6449  elovmpt3imp  6517  difsnexi  6592  ordsuc  6633  ordsucelsuc  6641  1stval  6786  2ndval  6787  1st2val  6810  2nd2val  6811  bropopvvv  6863  suppimacnv  6912  suppssdm  6914  ressuppss  6919  suppun  6920  extmptsuppeq  6924  funsssuppss  6926  fczsupp0  6929  suppss  6930  suppssov1  6932  suppss2  6934  suppssfv  6936  supp0cosupp0  6939  imacosupp  6940  mpt2xopynvov0  6946  mpt2xopoveqd  6949  pwuninel  7004  smofvon2  7027  om0x  7169  brdomg  7526  snfi  7596  sdomirr  7654  domunsn  7667  2pwuninel  7672  snnen2o  7706  suppeqfsuppbi  7843  fsuppun  7848  funsnfsupp  7853  fipwuni  7886  oicl  7954  oif  7955  wemapso2  7979  card2on  7980  en2lp  8030  tctr  8171  r1tr  8194  rankdmr1  8219  r1pw  8263  r1pwOLD  8264  rankuni  8281  scottex  8303  cardidm  8340  alephcard  8451  alephnbtwn  8452  cdacomen  8561  cfub  8629  cardcf  8632  cflecard  8633  cfle  8634  cflim2  8643  cfidm  8655  isf32lem9  8741  itunisuc  8799  itunitc1  8800  itunitc  8801  ituniiun  8802  axcc2lem  8816  alephreg  8957  pwcfsdom  8958  cfpwsdom  8959  axunndlem1  8970  axpownd  8978  tskmcl  9219  addcompi  9272  addasspi  9273  mulcompi  9274  mulasspi  9275  distrpi  9276  addnidpi  9279  nlt1pi  9284  addcompq  9328  addcomnq  9329  mulcompq  9330  mulcomnq  9331  adderpq  9334  mulerpq  9335  addassnq  9336  mulassnq  9337  distrnq  9339  genpass  9387  addcompr  9399  mulcompr  9401  distrpr  9406  ltexprlem7  9420  addcomsr  9464  addasssr  9465  mulcomsr  9466  mulasssr  9467  distrsr  9468  uzssz  11101  uzwo  11144  uzwoOLD  11145  nn01to3  11175  elixx3g  11542  iooid  11557  elfz2  11679  injresinjlem  11893  injresinj  11894  fleqceilz  11949  modifeq2int  12017  ltweuz  12040  fzofi  12052  fsuppmapnn0fiubex  12066  hashrabrsn  12408  hashrabsn01  12409  hashrabsn1  12410  elprchashprn2  12429  hashss  12439  hashsnlei  12443  hash1snb  12444  euhash1  12445  hashgt12el  12446  hashgt12el2  12447  hash2pwpr  12485  hashge2el2dif  12487  ccatsymb  12565  swrd00  12608  swrdnd  12620  swrd0  12621  swrdccatin1  12671  repswswrd  12719  0csh0  12727  cshwcl  12732  cshwidxmod  12737  repswcshw  12743  cshw1  12753  modfsummods  13570  gcdaddmlem  14025  pcmptcl  14269  cshwshash  14447  strfvss  14508  strfvi  14530  setsnid  14532  ressbas  14545  ressbasss  14547  resslem  14548  ress0  14549  ressress  14552  strle1  14586  0rest  14685  firest  14688  topnval  14690  xpsaddlem  14830  xpsvsca  14834  homffval  14947  comfffval  14954  oppchomfval  14970  oppcbas  14974  fullfunc  15133  fthfunc  15134  natfval  15173  fucbas  15187  fuchom  15188  arwval  15228  coafval  15249  xpcbas  15305  xpchomfval  15306  xpccofval  15309  lubfun  15467  glbfun  15480  oduval  15617  oduleval  15618  odumeet  15627  odujoin  15629  ipopos  15647  plusffval  15744  grpidval  15749  gsum0  15832  frmdplusg  15854  frmd0  15860  grpinvfval  15898  grpinvfvi  15901  grpsubfval  15902  mulgfval  15953  mulgfvi  15956  cntrval  16162  oppgval  16187  oppgplusfval  16188  symgbas  16210  symgplusg  16219  psgnfval  16331  odfval  16363  oppglsm  16468  efgval  16541  mgpval  16946  mgpplusg  16947  rngidval  16957  opprval  17074  opprmulfval  17075  dvdsrval  17095  invrfval  17123  dvrfval  17134  staffval  17296  scaffval  17330  rlmval  17637  rlmsca2  17647  2idlval  17680  rrgval  17734  asclfval  17782  psrplusg  17833  psrmulr  17836  psrvscafval  17842  mplval  17883  mplcoe3  17927  mplcoe3OLD  17928  evlval  17992  psr1val  18024  vr1val  18030  ply1val  18032  ply1basfvi  18081  ply1plusgfvi  18082  psr1sca2  18091  ply1sca2  18094  ply1ascl  18098  cply1mul  18134  gsummoncoe1  18145  evl1fval  18163  evl1fval1  18166  zrhval  18340  zlmlem  18349  zlmvsca  18354  chrval  18357  evpmss  18417  psgndiflemB  18431  ipffval  18478  thlbas  18522  thlle  18523  thloc  18525  pjfval  18532  dsmmval2  18562  mamufacex  18686  mavmulsolcl  18848  marrepfval  18857  marepvfval  18862  submafval  18876  mdetfval  18883  mdetfval1  18887  mdetunilem7  18915  mdetunilem8  18916  madufval  18934  minmar1fval  18943  mp2pm2mplem4  19105  tgdif0  19288  indislem  19295  resstopn  19481  iocpnfordt  19510  icomnfordt  19511  hmeofval  20022  ussval  20525  nmfval  20872  nghmfval  20992  pcofval  21273  tchval  21424  ioombl  21738  ibladdlem  21989  itgaddlem1  21992  iblabs  21998  limccnp2  22059  dvbsss  22069  perfdvf  22070  mdegfval  22223  deg1fval  22243  deg1fvi  22248  uc1pval  22303  mon1pval  22305  ttglem  23883  axcontlem12  23982  usgraedgprv  24080  usgra1v  24094  nbusgra  24132  nbgra0nb  24133  nbgranself2  24140  cusgra1v  24165  uvtxisvtx  24194  uvtx0  24195  uvtx01vtx  24196  1conngra  24379  wwlknfi  24442  wlk0  24465  clwwlkprop  24474  clwwlkgt0  24475  clwwlknprop  24476  clwlkisclwwlklem2a4  24488  2wlkonot3v  24579  2spthonot3v  24580  vdgrf  24602  nbhashuvtx1  24619  frgra2v  24703  1to2vfriswmgra  24710  2pthfrgra  24715  frgrancvvdeqlem2  24736  2spotdisj  24766  2spotiundisj  24767  2spotmdisj  24773  frgrareggt1  24821  frgrareg  24822  frgraregord013  24823  frgraogt3nreg  24825  friendship  24827  avril1  24875  ismgm  25026  vafval  25200  bafval  25201  smfval  25202  vsfval  25232  bcsiALT  25800  resvsca  27511  resvlem  27512  cntnevol  27867  signsw0glem  28178  dfrdg3  28834  trpredlem1  28915  bdayelon  29045  fvsingle  29175  unisnif  29180  funpartfv  29200  fullfunfv  29202  linedegen  29398  wl-nfs1t  29596  wl-sbcom3  29640  itg2addnclem  29671  ibladdnclem  29676  itgaddnclem1  29678  iblabsnc  29684  iblmulc2nc  29685  ftc1anclem5  29699  ftc1anclem8  29702  tsim2  30170  tsim3  30171  tsbi1  30172  tsbi2  30173  tsbi3  30174  tsan2  30181  tsan3  30182  tsor2  30187  tsor3  30188  ac6s6  30212  mzpmfp  30311  mzpmfpOLD  30312  itgocn  30746  mendbas  30766  mendplusgfval  30767  mendmulrfval  30769  mendsca  30771  mendvscafval  30772  arearect  30816  areaquad  30817  addcomgi  30971  sqwvfoura  31557  sqwvfourb  31558  fourierswlem  31559  fouriersw  31560  tz6.12-afv  31753  ndmaovcl  31783  otiunsndisjX  31796  pgrpgt2nabl  32056  suppmptcfin  32071  linc1  32125  lindslinindsimp2lem5  32162  ax6e2ndeq  32430  2sb5ndVD  32808  2sb5ndALT  32830  bnj1189  33162  bj-dfif5ALT  33248  bj-ifid  33253  bj-elimhyp  33258  bj-ax12v  33447  bj-hbs1  33451  bj-dtru  33482  bj-nfcsym  33559  bj-inftyexpidisj  33703  xptrrel  36803