Theorem pm2.61i 167

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 23	. 2 |- ( ph -> ph )
2		pm2.61i.2	. . 3 |- ( -. ph -> ps )
3		pm2.61i.1	. . 3 |- ( ph -> ps )
4	2, 3	ja 164	. 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  168  pm2.61nii  169  pm2.61iii  170  pm2.65i  176  pm5.21nii  354  pm5.18  357  biass  360  pm2.61ian  797  ecase3  949  4cases  957  elimh  964  pm4.42  968  3ecase  1369  ifpid  1433  ax6e  2058  exdistrf  2131  equvini  2143  dfsb2  2168  sbequi  2170  sbi1  2187  sbcom3  2206  sbco2  2210  sbco3  2212  sb9  2221  ax12vALT  2223  hbs1  2232  nfsb  2236  2ax6e  2246  sbal  2258  eujustALT  2269  pm2.61ine  2744  pm2.61neOLD  2747  rgen2aOLD  2860  ralcom2  3000  eueq2  3251  moeq3  3254  mo2icl  3256  sbc2or  3314  sbcimdv  3367  unineq  3729  csb0  3805  sbcel12  3806  sbcne12  3809  sbcel2  3812  csbidm  3825  csbun  3832  csbin  3833  ralidm  3907  ifsb  3928  ifid  3952  ifnot  3960  ifan  3961  ifor  3962  csbif  3965  elimhyp  3973  elimhyp2v  3974  elimhyp3v  3975  elimhyp4v  3976  elimdhyp  3978  keephyp2v  3980  keephyp3v  3981  eqoreldif  4044  rabsnif  4072  tppreqb  4144  ssunsn2  4162  dfopif  4187  csbuni  4250  sbcbr123  4477  sbcbr  4478  unisn2  4561  intabs  4586  class2set  4592  snexALT  4611  dtru  4616  dtruALT  4654  snex  4663  dtruALT2  4666  copsexg  4707  otsndisj  4726  otiunsndisj  4727  csbopab  4753  dfid3  4770  csbxp  4936  csbres  5128  csbima12  5205  soirri  5246  csbrn  5317  dmsnopss  5328  dmsnsnsn  5334  opswap  5343  unixpid  5391  nsuceq0  5522  ordsssuc2  5530  iotassuni  5581  iotaex  5582  dfiota4  5593  csbiota  5594  dffv3  5877  fvrn0  5903  ndmfv  5905  fveqres  5915  csbfv12  5916  csbfv  5918  dffv2  5954  fvco4i  5959  fvmptss  5974  fvmptex  5976  fvmptss2  5985  f0cli  6048  fvunsn  6111  fconst5  6137  csbriota  6279  riotassuni  6303  csbov123  6339  csbov  6340  0neqopab  6349  elimdelov  6386  ovif12  6389  ndmovcl  6468  ndmovord  6473  elovmpt3imp  6538  difsnexi  6613  ordsuc  6655  ordsucelsuc  6663  1stval  6809  2ndval  6810  1st2val  6833  2nd2val  6834  bropopvvv  6887  suppimacnv  6936  suppssdm  6938  ressuppss  6945  suppun  6946  extmptsuppeq  6950  funsssuppss  6952  fczsupp0  6955  suppss  6956  suppssov1  6958  suppss2  6960  suppssfv  6962  supp0cosupp0  6965  imacosupp  6966  mpt2xopynvov0  6972  mpt2xopoveqd  6975  pwuninel  7030  smofvon2  7083  om0x  7229  brdomg  7587  snfi  7657  sdomirr  7715  domunsn  7728  2pwuninel  7733  snnen2o  7767  suppeqfsuppbi  7903  fsuppun  7908  funsnfsupp  7913  fipwuni  7946  oicl  8044  oif  8045  wemapso2  8068  card2on  8069  en2lp  8118  tctr  8223  r1tr  8246  rankdmr1  8271  r1pw  8315  r1pwALT  8316  rankuni  8333  scottex  8355  cardidm  8392  alephcard  8499  alephnbtwn  8500  cdacomen  8609  cfub  8677  cardcf  8680  cflecard  8681  cfle  8682  cflim2  8691  cfidm  8703  isf32lem9  8789  itunisuc  8847  itunitc1  8848  itunitc  8849  ituniiun  8850  axcc2lem  8864  alephreg  9005  pwcfsdom  9006  cfpwsdom  9007  axunndlem1  9018  axpownd  9024  tskmcl  9265  addcompi  9318  addasspi  9319  mulcompi  9320  mulasspi  9321  distrpi  9322  addnidpi  9325  nlt1pi  9330  addcompq  9374  addcomnq  9375  mulcompq  9376  mulcomnq  9377  adderpq  9380  mulerpq  9381  addassnq  9382  mulassnq  9383  distrnq  9385  genpass  9433  addcompr  9445  mulcompr  9447  distrpr  9452  ltexprlem7  9466  addcomsr  9510  addasssr  9511  mulcomsr  9512  mulasssr  9513  distrsr  9514  uzssz  11178  uzwo  11222  nn01to3  11257  elixx3g  11648  iooid  11664  elfz2  11789  injresinjlem  12021  injresinj  12022  fleqceilz  12078  modifeq2int  12149  ltweuz  12172  fzofi  12184  fsuppmapnn0fiubex  12201  hashrabrsn  12548  hashrabsn01  12549  hashrabsn1  12550  elprchashprn2  12570  hashss  12583  hashsnlei  12587  hash1snb  12588  hashgt12el  12590  hashgt12el2  12591  hash2pwpr  12628  hashge2el2dif  12630  ccatsymb  12714  swrd00  12759  swrd0  12775  swrdccatin1  12824  repswswrd  12872  0csh0  12880  cshwcl  12885  cshwidxmod  12890  repswcshw  12896  cshw1  12906  xptrrel  13023  trclfvcotrg  13059  relexpfld  13091  modfsummods  13831  gcdaddmlem  14466  pcmptcl  14790  prmgaplem5  14979  prmgaplem6  14980  cshwshash  15029  strfvss  15093  strfvi  15117  setsnid  15119  ressbas  15132  ressbasss  15134  resslem  15135  ress0  15136  ressress  15140  strle1  15174  0rest  15278  firest  15281  topnval  15283  xpsaddlem  15423  xpsvsca  15427  homffval  15537  comfffval  15545  oppchomfval  15561  oppcbas  15565  fullfunc  15753  fthfunc  15754  natfval  15793  fucbas  15807  fuchom  15808  arwval  15880  coafval  15901  xpcbas  16005  xpchomfval  16006  xpccofval  16009  lubfun  16168  glbfun  16181  oduval  16318  oduleval  16319  odumeet  16328  odujoin  16330  ipopos  16348  plusffval  16435  grpidval  16445  gsum0  16463  frmdplusg  16580  frmd0  16586  mgm2nsgrplem2  16595  mgm2nsgrplem3  16596  sgrp2rid2  16602  grpinvfval  16646  grpinvfvi  16649  grpsubfval  16650  mulgfval  16701  mulgfvi  16704  cntrval  16915  oppgval  16940  oppgplusfval  16941  symgbas  16963  symgplusg  16972  psgnfval  17083  odfval  17115  oppglsm  17220  efgval  17293  mgpval  17652  mgpplusg  17653  ringidval  17663  opprval  17778  opprmulfval  17779  dvdsrval  17799  invrfval  17827  dvrfval  17838  staffval  18001  scaffval  18035  rlmval  18340  rlmsca2  18350  2idlval  18383  rrgval  18437  asclfval  18484  psrplusg  18531  psrmulr  18534  psrvscafval  18540  mplval  18578  mplcoe3  18616  evlval  18673  psr1val  18705  vr1val  18711  ply1val  18713  ply1basfvi  18760  ply1plusgfvi  18761  psr1sca2  18770  ply1sca2  18773  ply1ascl  18777  cply1mul  18813  gsummoncoe1  18824  evl1fval  18842  evl1fval1  18845  zrhval  19001  zlmlem  19010  zlmvsca  19015  chrval  19018  evpmss  19076  psgndiflemB  19090  ipffval  19137  thlbas  19181  thlle  19182  thloc  19184  pjfval  19191  dsmmval2  19221  mamufacex  19336  mavmulsolcl  19498  marrepfval  19507  marepvfval  19512  submafval  19526  mdetfval  19533  mdetfval1  19537  mdetunilem7  19565  mdetunilem8  19566  madufval  19584  minmar1fval  19593  mp2pm2mplem4  19755  tgdif0  19930  indislem  19937  resstopn  20124  iocpnfordt  20153  icomnfordt  20154  hmeofval  20695  ussval  21196  nmfval  21525  nghmfval  21645  pcofval  21925  tchval  22076  ioombl  22386  ibladdlem  22645  itgaddlem1  22648  iblabs  22654  dvbsss  22725  perfdvf  22726  mdegfval  22879  deg1fval  22897  deg1fvi  22902  uc1pval  22956  mon1pval  22958  ttglem  24743  axcontlem12  24842  usgraedgprv  24940  usgra1v  24954  nbusgra  24992  nbgra0nb  24993  nbgranself2  25000  cusgra1v  25025  uvtxisvtx  25054  uvtx0  25055  uvtx01vtx  25056  1conngra  25239  wwlknfi  25302  wlk0  25325  clwwlkprop  25334  clwwlkgt0  25335  clwwlknprop  25336  clwlkisclwwlklem2a4  25348  2wlkonot3v  25439  2spthonot3v  25440  vdgrf  25462  nbhashuvtx1  25479  frgra2v  25563  1to2vfriswmgra  25570  2pthfrgra  25575  frgrancvvdeqlem2  25595  2spotdisj  25625  2spotiundisj  25626  2spotmdisj  25632  frgrareggt1  25680  frgrareg  25681  frgraregord013  25682  frgraogt3nreg  25684  friendship  25686  avril1  25736  ismgmOLD  25884  vafval  26058  bafval  26059  smfval  26060  vsfval  26090  bcsiALT  26658  resvsca  28423  resvlem  28424  cntnevol  28880  signsw0glem  29221  bnj1189  29597  mvtval  29917  mexval  29919  mexval2  29920  mdvval  29921  mrsubfval  29925  mrsubrn  29930  msubfval  29941  elmsubrn  29945  msubrn  29946  mvhfval  29950  mpstval  29952  msrfval  29954  mstaval  29961  mppsval  29989  mthmval  29992  dfrdg3  30221  trpredlem1  30246  bdayelon  30345  fvsingle  30463  unisnif  30468  funpartfv  30488  fullfunfv  30490  linedegen  30686  bj-elimhyp  30929  bj-ax12v  31119  bj-hbs1  31123  bj-dtru  31154  bj-nfcsym  31235  bj-inftyexpidisj  31388  csbdif  31461  wl-nfs1t  31569  wl-ax12  31607  wl-sbcom3  31619  itg2addnclem  31687  ibladdnclem  31692  itgaddnclem1  31694  iblabsnc  31700  iblmulc2nc  31701  ftc1anclem8  31718  tsbi1  32069  tsbi2  32070  ac6s6  32109  ax12  32174  equid1  32177  equid1ALT  32195  dvelimf-o  32199  ax12inda2ALT  32216  ax12inda2  32217  mzpmfp  35288  itgocn  35719  mendbas  35739  mendplusgfval  35740  mendmulrfval  35742  mendsca  35744  mendvscafval  35745  arearect  35789  areaquad  35790  addcomgi  36436  ax6e2ndeq  36553  2sb5ndVD  36937  2sb5ndALT  36959  sqwvfoura  37650  sqwvfourb  37651  fourierswlem  37652  fouriersw  37653  tz6.12-afv  38055  ndmaovcl  38085  nltle2tri  38096  fzopredsuc  38100  iccpartiltu  38116  iccpartigtl  38117  iccpartlt  38118  icceuelpartlem  38129  iccpartnel  38132  evenprm2  38222  stgoldbwt  38257  pfx00  38305  pfx0  38306  otiunsndisjX  38368  nzerooringczr  38822  pgrpgt2nabl  38901  suppmptcfin  38914  linc1  38968  lindslinindsimp2lem5  39005