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 22	. 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  2060  exdistrf  2134  equvini  2146  dfsb2  2171  sbequi  2173  sbi1  2190  sbcom3  2209  sbco2  2213  sbco3  2215  sb9  2224  ax12vALT  2226  hbs1  2235  nfsb  2239  2ax6e  2249  sbal  2261  eujustALT  2272  pm2.61ine  2733  pm2.61neOLD  2736  rgen2aOLD  2850  ralcom2  2990  eueq2  3244  moeq3  3247  mo2icl  3249  sbc2or  3308  sbcimdv  3361  unineq  3723  csb0  3801  sbcel12  3802  sbcne12  3805  sbcel2  3808  csbidm  3821  csbun  3828  csbin  3829  ralidm  3903  ifsb  3924  ifid  3948  ifnot  3956  ifan  3957  ifor  3958  csbif  3961  elimhyp  3969  elimhyp2v  3970  elimhyp3v  3971  elimhyp4v  3972  elimdhyp  3974  keephyp2v  3976  keephyp3v  3977  eqoreldif  4041  rabsnif  4069  tppreqb  4141  ssunsn2  4159  dfopif  4184  csbuni  4247  sbcbr123  4475  sbcbr  4476  unisn2  4560  intabs  4585  class2set  4591  snexALT  4610  dtru  4615  dtruALT  4653  snex  4662  dtruALT2  4665  copsexg  4706  otsndisj  4725  otiunsndisj  4726  csbopab  4752  dfid3  4769  csbxp  4935  csbres  5127  csbima12  5204  soirri  5245  csbrn  5316  dmsnopss  5327  dmsnsnsn  5333  opswap  5342  unixpid  5390  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  6975  mpt2xopoveqd  6978  pwuninel  7033  smofvon2  7086  om0x  7232  brdomg  7590  snfi  7660  sdomirr  7718  domunsn  7731  2pwuninel  7736  snnen2o  7770  suppeqfsuppbi  7906  fsuppun  7911  funsnfsupp  7916  fipwuni  7949  oicl  8053  oif  8054  wemapso2  8077  card2on  8078  en2lp  8127  tctr  8232  r1tr  8255  rankdmr1  8280  r1pw  8324  r1pwALT  8325  rankuni  8342  scottex  8364  cardidm  8401  alephcard  8508  alephnbtwn  8509  cdacomen  8618  cfub  8686  cardcf  8689  cflecard  8690  cfle  8691  cflim2  8700  cfidm  8712  isf32lem9  8798  itunisuc  8856  itunitc1  8857  itunitc  8858  ituniiun  8859  axcc2lem  8873  alephreg  9014  pwcfsdom  9015  cfpwsdom  9016  axunndlem1  9027  axpownd  9033  tskmcl  9273  addcompi  9326  addasspi  9327  mulcompi  9328  mulasspi  9329  distrpi  9330  addnidpi  9333  nlt1pi  9338  addcompq  9382  addcomnq  9383  mulcompq  9384  mulcomnq  9385  adderpq  9388  mulerpq  9389  addassnq  9390  mulassnq  9391  distrnq  9393  genpass  9441  addcompr  9453  mulcompr  9455  distrpr  9460  ltexprlem7  9474  addcomsr  9518  addasssr  9519  mulcomsr  9520  mulasssr  9521  distrsr  9522  uzssz  11185  uzwo  11229  nn01to3  11264  elixx3g  11655  iooid  11671  elfz2  11798  injresinjlem  12030  injresinj  12031  fleqceilz  12087  modifeq2int  12158  ltweuz  12181  fzofi  12193  fsuppmapnn0fiubex  12210  hashrabrsn  12557  hashrabsn01  12558  hashrabsn1  12559  elprchashprn2  12579  hashss  12592  hashsnlei  12596  hash1snb  12597  hashgt12el  12599  hashgt12el2  12600  hash2pwpr  12639  hashge2el2dif  12641  ccatsymb  12731  swrd00  12776  swrd0  12792  swrdccatin1  12841  repswswrd  12889  0csh0  12897  cshwcl  12902  cshwidxmod  12907  repswcshw  12913  cshw1  12923  xptrrel  13044  trclfvcotrg  13080  relexpfld  13112  modfsummods  13852  gcdaddmlem  14491  pcmptcl  14835  prmgaplem5  15024  prmgaplem6  15025  cshwshash  15074  strfvss  15138  strfvi  15162  setsnid  15164  ressbas  15178  ressbasss  15180  resslem  15181  ress0  15182  ressress  15186  strle1  15220  0rest  15327  firest  15330  topnval  15332  xpsaddlem  15480  xpsvsca  15484  homffval  15594  comfffval  15602  oppchomfval  15618  oppcbas  15622  fullfunc  15810  fthfunc  15811  natfval  15850  fucbas  15864  fuchom  15865  arwval  15937  coafval  15958  xpcbas  16062  xpchomfval  16063  xpccofval  16066  lubfun  16225  glbfun  16238  oduval  16375  oduleval  16376  odumeet  16385  odujoin  16387  ipopos  16405  plusffval  16492  grpidval  16502  gsum0  16520  frmdplusg  16637  frmd0  16643  mgm2nsgrplem2  16652  mgm2nsgrplem3  16653  sgrp2rid2  16659  grpinvfval  16703  grpinvfvi  16706  grpsubfval  16707  mulgfval  16758  mulgfvi  16761  cntrval  16972  oppgval  16997  oppgplusfval  16998  symgbas  17020  symgplusg  17029  psgnfval  17140  odfval  17178  odfvalOLD  17181  oppglsm  17293  efgval  17366  mgpval  17725  mgpplusg  17726  ringidval  17736  opprval  17851  opprmulfval  17852  dvdsrval  17872  invrfval  17900  dvrfval  17911  staffval  18074  scaffval  18108  rlmval  18413  rlmsca2  18423  2idlval  18456  rrgval  18510  asclfval  18557  psrplusg  18604  psrmulr  18607  psrvscafval  18613  mplval  18651  mplcoe3  18689  evlval  18746  psr1val  18778  vr1val  18784  ply1val  18786  ply1basfvi  18833  ply1plusgfvi  18834  psr1sca2  18843  ply1sca2  18846  ply1ascl  18850  cply1mul  18886  gsummoncoe1  18897  evl1fval  18915  evl1fval1  18918  zrhval  19077  zlmlem  19086  zlmvsca  19091  chrval  19094  evpmss  19152  psgndiflemB  19166  ipffval  19213  thlbas  19257  thlle  19258  thloc  19260  pjfval  19267  dsmmval2  19297  mamufacex  19412  mavmulsolcl  19574  marrepfval  19583  marepvfval  19588  submafval  19602  mdetfval  19609  mdetfval1  19613  mdetunilem7  19641  mdetunilem8  19642  madufval  19660  minmar1fval  19669  mp2pm2mplem4  19831  tgdif0  20006  indislem  20013  resstopn  20200  iocpnfordt  20229  icomnfordt  20230  hmeofval  20771  ussval  21272  nmfval  21601  nghmfval  21725  nghmfvalOLD  21743  pcofval  22039  tchval  22190  ioombl  22516  ibladdlem  22775  itgaddlem1  22778  iblabs  22784  dvbsss  22855  perfdvf  22856  mdegfval  23009  deg1fval  23027  deg1fvi  23032  uc1pval  23088  mon1pval  23090  ttglem  24904  axcontlem12  25003  usgraedgprv  25101  usgra1v  25115  nbusgra  25154  nbgra0nb  25155  nbgranself2  25162  cusgra1v  25187  uvtxisvtx  25216  uvtx0  25217  uvtx01vtx  25218  1conngra  25401  wwlknfi  25464  wlk0  25487  clwwlkprop  25496  clwwlkgt0  25497  clwwlknprop  25498  clwlkisclwwlklem2a4  25510  2wlkonot3v  25601  2spthonot3v  25602  vdgrf  25624  nbhashuvtx1  25641  frgra2v  25725  1to2vfriswmgra  25732  2pthfrgra  25737  frgrancvvdeqlem2  25757  2spotdisj  25787  2spotiundisj  25788  2spotmdisj  25794  frgrareggt1  25842  frgrareg  25843  frgraregord013  25844  frgraogt3nreg  25846  friendship  25848  avril1  25898  ismgmOLD  26046  vafval  26220  bafval  26221  smfval  26222  vsfval  26252  bcsiALT  26830  resvsca  28601  resvlem  28602  cntnevol  29058  signsw0glem  29450  bnj1189  29826  mvtval  30146  mexval  30148  mexval2  30149  mdvval  30150  mrsubfval  30154  mrsubrn  30159  msubfval  30170  elmsubrn  30174  msubrn  30175  mvhfval  30179  mpstval  30181  msrfval  30183  mstaval  30190  mppsval  30218  mthmval  30221  dfrdg3  30450  trpredlem1  30475  bdayelon  30574  fvsingle  30692  unisnif  30697  funpartfv  30717  fullfunfv  30719  linedegen  30915  bj-elimhyp  31158  bj-ax12v  31347  bj-hbs1  31351  bj-dtru  31382  bj-nfcsym  31463  bj-inftyexpidisj  31616  csbdif  31690  finxpreclem4  31750  finxp00  31758  wl-nfs1t  31835  wl-ax12  31877  wl-sbcom3  31889  itg2addnclem  31957  ibladdnclem  31962  itgaddnclem1  31964  iblabsnc  31970  iblmulc2nc  31971  ftc1anclem8  31988  tsbi1  32339  tsbi2  32340  ac6s6  32379  ax12  32444  equid1  32447  equid1ALT  32465  dvelimf-o  32469  ax12inda2ALT  32486  ax12inda2  32487  mzpmfp  35558  itgocn  36000  mendbas  36020  mendplusgfval  36021  mendmulrfval  36023  mendsca  36025  mendvscafval  36026  arearect  36070  areaquad  36071  addcomgi  36779  ax6e2ndeq  36896  2sb5ndVD  37280  2sb5ndALT  37302  sqwvfoura  38032  sqwvfourb  38033  fourierswlem  38034  fouriersw  38035  tz6.12-afv  38545  ndmaovcl  38575  nltle2tri  38586  fzopredsuc  38590  iccpartiltu  38606  iccpartigtl  38607  iccpartlt  38608  icceuelpartlem  38619  iccpartnel  38622  evenprm2  38712  stgoldbwt  38747  pfx00  38795  pfx0  38796  n0snor2el  38862  otiunsndisjX  38871  usgr1v  39107  nbuhgr  39178  nbusgr  39182  uhgrnbgr0nb  39187  nbgr1vtx  39191  nbgrnself2  39196  uvtxa0  39225  sizusglecusg  39281  nzerooringczr  39694  pgrpgt2nabl  39773  suppmptcfin  39786  linc1  39840  lindslinindsimp2lem5  39877