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  790  ecase3  941  4cases  949  elimh  956  pm4.42  960  3ecase  1334  ax6e  1988  exdistrf  2061  equvini  2073  dfsb2  2100  sbequi  2102  sbi1  2119  sbcom3  2139  sbco2  2144  sbco3  2146  sb9  2155  ax12vALT  2157  hbs1  2166  nfsb  2170  2ax6e  2180  sbal  2192  ax12  2220  equid1  2223  equid1ALT  2241  dvelimf-o  2245  ax12inda2ALT  2262  ax12inda2  2263  eujustALT  2271  pm2.61ine  2756  pm2.61neOLD  2759  rgen2aOLD  2871  ralcom2  3008  eueq2  3259  moeq3  3262  mo2icl  3264  sbc2or  3322  sbcimdv  3382  unineq  3733  csb0  3808  sbcel12  3809  sbcne12  3813  sbcel2  3817  csbidm  3832  csbun  3843  csbin  3846  ralidm  3918  ifsb  3939  ifid  3963  ifnot  3971  ifan  3972  ifor  3973  csbif  3976  elimhyp  3985  elimhyp2v  3986  elimhyp3v  3987  elimhyp4v  3988  elimdhyp  3990  keephyp2v  3992  keephyp3v  3993  rabsnif  4084  tppreqb  4156  ssunsn2  4174  dfopif  4199  csbuni  4262  sbcbr123  4488  sbcbr  4490  unisn2  4573  intabs  4598  class2set  4604  snexALT  4623  dtru  4628  dtruALT  4669  snex  4678  dtruALT2  4681  copsexg  4722  copsexgOLD  4723  otsndisj  4742  otiunsndisj  4743  csbopab  4769  dfid3  4786  nsuceq0  4948  ordsssuc2  4956  csbxp  5071  csbres  5266  csbima12  5344  soirri  5383  soirriOLD  5388  csbrn  5458  dmsnopss  5470  dmsnsnsn  5476  opswap  5485  unixpid  5532  iotassuni  5557  iotaex  5558  dfiota4  5569  csbiota  5570  dffv3  5852  fvrn0  5878  ndmfv  5880  fveqres  5890  csbfv12  5891  csbfv  5894  dffv2  5931  fvco4i  5936  fvmptss  5949  fvmptex  5951  fvmptss2  5960  f0cli  6027  fvunsn  6088  fconst5  6113  csbriota  6254  riotassuniOLD  6279  csbov123  6315  csbov  6316  0neqopab  6326  elimdelov  6363  ovif12  6366  ndmovcl  6445  ndmovord  6450  elovmpt3imp  6518  difsnexi  6593  ordsuc  6634  ordsucelsuc  6642  1stval  6787  2ndval  6788  1st2val  6811  2nd2val  6812  bropopvvv  6865  suppimacnv  6914  suppssdm  6916  ressuppss  6921  suppun  6922  extmptsuppeq  6926  funsssuppss  6928  fczsupp0  6931  suppss  6932  suppssov1  6934  suppss2  6936  suppssfv  6938  supp0cosupp0  6941  imacosupp  6942  mpt2xopynvov0  6948  mpt2xopoveqd  6951  pwuninel  7006  smofvon2  7029  om0x  7171  brdomg  7528  snfi  7598  sdomirr  7656  domunsn  7669  2pwuninel  7674  snnen2o  7708  suppeqfsuppbi  7845  fsuppun  7850  funsnfsupp  7855  fipwuni  7888  oicl  7957  oif  7958  wemapso2  7982  card2on  7983  en2lp  8033  tctr  8174  r1tr  8197  rankdmr1  8222  r1pw  8266  r1pwOLD  8267  rankuni  8284  scottex  8306  cardidm  8343  alephcard  8454  alephnbtwn  8455  cdacomen  8564  cfub  8632  cardcf  8635  cflecard  8636  cfle  8637  cflim2  8646  cfidm  8658  isf32lem9  8744  itunisuc  8802  itunitc1  8803  itunitc  8804  ituniiun  8805  axcc2lem  8819  alephreg  8960  pwcfsdom  8961  cfpwsdom  8962  axunndlem1  8973  axpownd  8981  tskmcl  9222  addcompi  9275  addasspi  9276  mulcompi  9277  mulasspi  9278  distrpi  9279  addnidpi  9282  nlt1pi  9287  addcompq  9331  addcomnq  9332  mulcompq  9333  mulcomnq  9334  adderpq  9337  mulerpq  9338  addassnq  9339  mulassnq  9340  distrnq  9342  genpass  9390  addcompr  9402  mulcompr  9404  distrpr  9409  ltexprlem7  9423  addcomsr  9467  addasssr  9468  mulcomsr  9469  mulasssr  9470  distrsr  9471  uzssz  11109  uzwo  11153  uzwoOLD  11154  nn01to3  11184  elixx3g  11551  iooid  11566  elfz2  11688  injresinjlem  11904  injresinj  11905  fleqceilz  11960  modifeq2int  12028  ltweuz  12051  fzofi  12063  fsuppmapnn0fiubex  12077  hashrabrsn  12419  hashrabsn01  12420  hashrabsn1  12421  elprchashprn2  12440  hashss  12453  hashsnlei  12457  hash1snb  12458  hashgt12el  12460  hashgt12el2  12461  hash2pwpr  12498  hashge2el2dif  12500  ccatsymb  12579  swrd00  12624  swrdnd  12636  swrd0  12637  swrdccatin1  12687  repswswrd  12735  0csh0  12743  cshwcl  12748  cshwidxmod  12753  repswcshw  12759  cshw1  12769  modfsummods  13586  gcdaddmlem  14043  pcmptcl  14287  cshwshash  14466  strfvss  14527  strfvi  14549  setsnid  14551  ressbas  14564  ressbasss  14566  resslem  14567  ress0  14568  ressress  14571  strle1  14605  0rest  14704  firest  14707  topnval  14709  xpsaddlem  14849  xpsvsca  14853  homffval  14963  comfffval  14970  oppchomfval  14986  oppcbas  14990  fullfunc  15149  fthfunc  15150  natfval  15189  fucbas  15203  fuchom  15204  arwval  15244  coafval  15265  xpcbas  15321  xpchomfval  15322  xpccofval  15325  lubfun  15484  glbfun  15497  oduval  15634  oduleval  15635  odumeet  15644  odujoin  15646  ipopos  15664  plusffval  15751  grpidval  15761  gsum0  15779  frmdplusg  15896  frmd0  15902  mgm2nsgrplem2  15911  mgm2nsgrplem3  15912  sgrp2rid2  15918  grpinvfval  15962  grpinvfvi  15965  grpsubfval  15966  mulgfval  16017  mulgfvi  16020  cntrval  16231  oppgval  16256  oppgplusfval  16257  symgbas  16279  symgplusg  16288  psgnfval  16399  odfval  16431  oppglsm  16536  efgval  16609  mgpval  17018  mgpplusg  17019  ringidval  17029  opprval  17147  opprmulfval  17148  dvdsrval  17168  invrfval  17196  dvrfval  17207  staffval  17370  scaffval  17404  rlmval  17711  rlmsca2  17721  2idlval  17755  rrgval  17809  asclfval  17857  psrplusg  17908  psrmulr  17911  psrvscafval  17917  mplval  17958  mplcoe3  18002  mplcoe3OLD  18003  evlval  18067  psr1val  18099  vr1val  18105  ply1val  18107  ply1basfvi  18156  ply1plusgfvi  18157  psr1sca2  18166  ply1sca2  18169  ply1ascl  18173  cply1mul  18209  gsummoncoe1  18220  evl1fval  18238  evl1fval1  18241  zrhval  18418  zlmlem  18427  zlmvsca  18432  chrval  18435  evpmss  18495  psgndiflemB  18509  ipffval  18556  thlbas  18600  thlle  18601  thloc  18603  pjfval  18610  dsmmval2  18640  mamufacex  18764  mavmulsolcl  18926  marrepfval  18935  marepvfval  18940  submafval  18954  mdetfval  18961  mdetfval1  18965  mdetunilem7  18993  mdetunilem8  18994  madufval  19012  minmar1fval  19021  mp2pm2mplem4  19183  tgdif0  19367  indislem  19374  resstopn  19560  iocpnfordt  19589  icomnfordt  19590  hmeofval  20132  ussval  20635  nmfval  20982  nghmfval  21102  pcofval  21383  tchval  21534  ioombl  21848  ibladdlem  22099  itgaddlem1  22102  iblabs  22108  dvbsss  22179  perfdvf  22180  mdegfval  22333  deg1fval  22353  deg1fvi  22358  uc1pval  22413  mon1pval  22415  ttglem  24051  axcontlem12  24150  usgraedgprv  24248  usgra1v  24262  nbusgra  24300  nbgra0nb  24301  nbgranself2  24308  cusgra1v  24333  uvtxisvtx  24362  uvtx0  24363  uvtx01vtx  24364  1conngra  24547  wwlknfi  24610  wlk0  24633  clwwlkprop  24642  clwwlkgt0  24643  clwwlknprop  24644  clwlkisclwwlklem2a4  24656  2wlkonot3v  24747  2spthonot3v  24748  vdgrf  24770  nbhashuvtx1  24787  frgra2v  24871  1to2vfriswmgra  24878  2pthfrgra  24883  frgrancvvdeqlem2  24903  2spotdisj  24933  2spotiundisj  24934  2spotmdisj  24940  frgrareggt1  24988  frgrareg  24989  frgraregord013  24990  frgraogt3nreg  24992  friendship  24994  avril1  25043  ismgmOLD  25194  vafval  25368  bafval  25369  smfval  25370  vsfval  25400  bcsiALT  25968  resvsca  27693  resvlem  27694  cntnevol  28072  signsw0glem  28383  mvtval  28733  mexval  28735  mexval2  28736  mdvval  28737  mrsubfval  28741  mrsubrn  28746  msubfval  28757  elmsubrn  28761  msubrn  28762  mvhfval  28766  mpstval  28768  msrfval  28770  mstaval  28777  mppsval  28805  mthmval  28808  dfrdg3  29204  trpredlem1  29285  bdayelon  29415  fvsingle  29545  unisnif  29550  funpartfv  29570  fullfunfv  29572  linedegen  29768  wl-nfs1t  29966  wl-sbcom3  30010  itg2addnclem  30041  ibladdnclem  30046  itgaddnclem1  30048  iblabsnc  30054  iblmulc2nc  30055  ftc1anclem8  30072  tsbi1  30515  tsbi2  30516  ac6s6  30555  mzpmfp  30654  mzpmfpOLD  30655  itgocn  31089  mendbas  31109  mendplusgfval  31110  mendmulrfval  31112  mendsca  31114  mendvscafval  31115  arearect  31159  areaquad  31160  addcomgi  31319  sqwvfoura  31900  sqwvfourb  31901  fourierswlem  31902  fouriersw  31903  tz6.12-afv  32096  ndmaovcl  32126  otiunsndisjX  32139  pgrpgt2nabl  32687  suppmptcfin  32702  linc1  32756  lindslinindsimp2lem5  32793  ax6e2ndeq  33060  2sb5ndVD  33438  2sb5ndALT  33460  bnj1189  33793  bj-dfif5ALT  33891  bj-ifid  33896  bj-elimhyp  33901  bj-ax12v  34090  bj-hbs1  34094  bj-dtru  34125  bj-nfcsym  34202  bj-inftyexpidisj  34347  xptrrel  37462