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  351  pm5.18  354  biass  357  pm2.61ian  788  ecase3  939  4cases  947  elimh  954  pm4.42  958  3ecase  1331  ifpid  1395  ax6e  2009  exdistrf  2081  equvini  2093  dfsb2  2118  sbequi  2120  sbi1  2137  sbcom3  2157  sbco2  2162  sbco3  2164  sb9  2173  ax12vALT  2175  hbs1  2184  nfsb  2188  2ax6e  2198  sbal  2210  eujustALT  2221  pm2.61ine  2695  pm2.61neOLD  2698  rgen2aOLD  2810  ralcom2  2947  eueq2  3198  moeq3  3201  mo2icl  3203  sbc2or  3261  sbcimdv  3314  unineq  3673  csb0  3749  sbcel12  3750  sbcne12  3753  sbcel2  3756  csbidm  3769  csbun  3776  csbin  3777  ralidm  3849  ifsb  3870  ifid  3894  ifnot  3902  ifan  3903  ifor  3904  csbif  3907  elimhyp  3915  elimhyp2v  3916  elimhyp3v  3917  elimhyp4v  3918  elimdhyp  3920  keephyp2v  3922  keephyp3v  3923  rabsnif  4013  tppreqb  4085  ssunsn2  4103  dfopif  4128  csbuni  4191  sbcbr123  4418  sbcbr  4419  unisn2  4501  intabs  4526  class2set  4532  snexALT  4551  dtru  4556  dtruALT  4594  snex  4603  dtruALT2  4606  copsexg  4647  otsndisj  4666  otiunsndisj  4667  csbopab  4693  dfid3  4710  nsuceq0  4872  ordsssuc2  4880  csbxp  4995  csbres  5189  csbima12  5266  soirri  5306  csbrn  5377  dmsnopss  5388  dmsnsnsn  5394  opswap  5403  unixpid  5451  iotassuni  5476  iotaex  5477  dfiota4  5488  csbiota  5489  dffv3  5770  fvrn0  5796  ndmfv  5798  fveqres  5808  csbfv12  5809  csbfv  5811  dffv2  5847  fvco4i  5852  fvmptss  5866  fvmptex  5868  fvmptss2  5877  f0cli  5944  fvunsn  6005  fconst5  6031  csbriota  6170  riotassuni  6194  csbov123  6230  csbov  6231  0neqopab  6240  elimdelov  6277  ovif12  6280  ndmovcl  6359  ndmovord  6364  elovmpt3imp  6432  difsnexi  6507  ordsuc  6548  ordsucelsuc  6556  1stval  6701  2ndval  6702  1st2val  6725  2nd2val  6726  bropopvvv  6779  suppimacnv  6828  suppssdm  6830  ressuppss  6837  suppun  6838  extmptsuppeq  6842  funsssuppss  6844  fczsupp0  6847  suppss  6848  suppssov1  6850  suppss2  6852  suppssfv  6854  supp0cosupp0  6857  imacosupp  6858  mpt2xopynvov0  6864  mpt2xopoveqd  6867  pwuninel  6922  smofvon2  6945  om0x  7087  brdomg  7445  snfi  7515  sdomirr  7573  domunsn  7586  2pwuninel  7591  snnen2o  7625  suppeqfsuppbi  7758  fsuppun  7763  funsnfsupp  7768  fipwuni  7801  oicl  7869  oif  7870  wemapso2  7894  card2on  7895  en2lp  7944  tctr  8084  r1tr  8107  rankdmr1  8132  r1pw  8176  r1pwALT  8177  rankuni  8194  scottex  8216  cardidm  8253  alephcard  8364  alephnbtwn  8365  cdacomen  8474  cfub  8542  cardcf  8545  cflecard  8546  cfle  8547  cflim2  8556  cfidm  8568  isf32lem9  8654  itunisuc  8712  itunitc1  8713  itunitc  8714  ituniiun  8715  axcc2lem  8729  alephreg  8870  pwcfsdom  8871  cfpwsdom  8872  axunndlem1  8883  axpownd  8889  tskmcl  9130  addcompi  9183  addasspi  9184  mulcompi  9185  mulasspi  9186  distrpi  9187  addnidpi  9190  nlt1pi  9195  addcompq  9239  addcomnq  9240  mulcompq  9241  mulcomnq  9242  adderpq  9245  mulerpq  9246  addassnq  9247  mulassnq  9248  distrnq  9250  genpass  9298  addcompr  9310  mulcompr  9312  distrpr  9317  ltexprlem7  9331  addcomsr  9375  addasssr  9376  mulcomsr  9377  mulasssr  9378  distrsr  9379  uzssz  11020  uzwo  11064  nn01to3  11094  elixx3g  11463  iooid  11478  elfz2  11600  injresinjlem  11824  injresinj  11825  fleqceilz  11881  modifeq2int  11952  ltweuz  11975  fzofi  11987  fsuppmapnn0fiubex  12001  hashrabrsn  12343  hashrabsn01  12344  hashrabsn1  12345  elprchashprn2  12365  hashss  12378  hashsnlei  12382  hash1snb  12383  hashgt12el  12385  hashgt12el2  12386  hash2pwpr  12423  hashge2el2dif  12425  ccatsymb  12509  swrd00  12554  swrd0  12570  swrdccatin1  12619  repswswrd  12667  0csh0  12675  cshwcl  12680  cshwidxmod  12685  repswcshw  12691  cshw1  12701  xptrrel  12818  trclfvcotrg  12854  relexpfld  12884  modfsummods  13609  gcdaddmlem  14168  pcmptcl  14412  cshwshash  14591  strfvss  14652  strfvi  14676  setsnid  14678  ressbas  14691  ressbasss  14693  resslem  14694  ress0  14695  ressress  14699  strle1  14733  0rest  14837  firest  14840  topnval  14842  xpsaddlem  14982  xpsvsca  14986  homffval  15096  comfffval  15104  oppchomfval  15120  oppcbas  15124  fullfunc  15312  fthfunc  15313  natfval  15352  fucbas  15366  fuchom  15367  arwval  15439  coafval  15460  xpcbas  15564  xpchomfval  15565  xpccofval  15568  lubfun  15727  glbfun  15740  oduval  15877  oduleval  15878  odumeet  15887  odujoin  15889  ipopos  15907  plusffval  15994  grpidval  16004  gsum0  16022  frmdplusg  16139  frmd0  16145  mgm2nsgrplem2  16154  mgm2nsgrplem3  16155  sgrp2rid2  16161  grpinvfval  16205  grpinvfvi  16208  grpsubfval  16209  mulgfval  16260  mulgfvi  16263  cntrval  16474  oppgval  16499  oppgplusfval  16500  symgbas  16522  symgplusg  16531  psgnfval  16642  odfval  16674  oppglsm  16779  efgval  16852  mgpval  17257  mgpplusg  17258  ringidval  17268  opprval  17386  opprmulfval  17387  dvdsrval  17407  invrfval  17435  dvrfval  17446  staffval  17609  scaffval  17643  rlmval  17950  rlmsca2  17960  2idlval  17994  rrgval  18048  asclfval  18096  psrplusg  18147  psrmulr  18150  psrvscafval  18156  mplval  18197  mplcoe3  18241  mplcoe3OLD  18242  evlval  18306  psr1val  18338  vr1val  18344  ply1val  18346  ply1basfvi  18395  ply1plusgfvi  18396  psr1sca2  18405  ply1sca2  18408  ply1ascl  18412  cply1mul  18448  gsummoncoe1  18459  evl1fval  18477  evl1fval1  18480  zrhval  18638  zlmlem  18647  zlmvsca  18652  chrval  18655  evpmss  18713  psgndiflemB  18727  ipffval  18774  thlbas  18818  thlle  18819  thloc  18821  pjfval  18828  dsmmval2  18858  mamufacex  18976  mavmulsolcl  19138  marrepfval  19147  marepvfval  19152  submafval  19166  mdetfval  19173  mdetfval1  19177  mdetunilem7  19205  mdetunilem8  19206  madufval  19224  minmar1fval  19233  mp2pm2mplem4  19395  tgdif0  19579  indislem  19586  resstopn  19773  iocpnfordt  19802  icomnfordt  19803  hmeofval  20344  ussval  20847  nmfval  21194  nghmfval  21314  pcofval  21595  tchval  21746  ioombl  22060  ibladdlem  22311  itgaddlem1  22314  iblabs  22320  dvbsss  22391  perfdvf  22392  mdegfval  22545  deg1fval  22565  deg1fvi  22570  uc1pval  22625  mon1pval  22627  ttglem  24300  axcontlem12  24399  usgraedgprv  24497  usgra1v  24511  nbusgra  24549  nbgra0nb  24550  nbgranself2  24557  cusgra1v  24582  uvtxisvtx  24611  uvtx0  24612  uvtx01vtx  24613  1conngra  24796  wwlknfi  24859  wlk0  24882  clwwlkprop  24891  clwwlkgt0  24892  clwwlknprop  24893  clwlkisclwwlklem2a4  24905  2wlkonot3v  24996  2spthonot3v  24997  vdgrf  25019  nbhashuvtx1  25036  frgra2v  25120  1to2vfriswmgra  25127  2pthfrgra  25132  frgrancvvdeqlem2  25152  2spotdisj  25182  2spotiundisj  25183  2spotmdisj  25189  frgrareggt1  25237  frgrareg  25238  frgraregord013  25239  frgraogt3nreg  25241  friendship  25243  avril1  25292  ismgmOLD  25439  vafval  25613  bafval  25614  smfval  25615  vsfval  25645  bcsiALT  26213  resvsca  27974  resvlem  27975  cntnevol  28355  signsw0glem  28693  mvtval  29049  mexval  29051  mexval2  29052  mdvval  29053  mrsubfval  29057  mrsubrn  29062  msubfval  29073  elmsubrn  29077  msubrn  29078  mvhfval  29082  mpstval  29084  msrfval  29086  mstaval  29093  mppsval  29121  mthmval  29124  dfrdg3  29394  trpredlem1  29475  bdayelon  29605  fvsingle  29723  unisnif  29728  funpartfv  29748  fullfunfv  29750  linedegen  29946  wl-nfs1t  30156  wl-sbcom3  30200  itg2addnclem  30232  ibladdnclem  30237  itgaddnclem1  30239  iblabsnc  30245  iblmulc2nc  30246  ftc1anclem8  30263  tsbi1  30706  tsbi2  30707  ac6s6  30746  mzpmfp  30845  itgocn  31281  mendbas  31301  mendplusgfval  31302  mendmulrfval  31304  mendsca  31306  mendvscafval  31307  arearect  31351  areaquad  31352  addcomgi  31533  sqwvfoura  32177  sqwvfourb  32178  fourierswlem  32179  fouriersw  32180  tz6.12-afv  32424  ndmaovcl  32454  pfx00  32559  pfx0  32560  otiunsndisjX  32622  nzerooringczr  33080  pgrpgt2nabl  33159  suppmptcfin  33172  linc1  33226  lindslinindsimp2lem5  33263  ax6e2ndeq  33672  2sb5ndVD  34057  2sb5ndALT  34079  bnj1189  34412  bj-elimhyp  34507  bj-ax12v  34695  bj-hbs1  34699  bj-dtru  34730  bj-nfcsym  34807  bj-inftyexpidisj  34960  ax12  35047  equid1  35050  equid1ALT  35068  dvelimf-o  35072  ax12inda2ALT  35089  ax12inda2  35090