Theorem pm2.61i 169

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 166	. 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  170  pm2.61nii  171  pm2.61iii  172  pm2.65i  178  pm5.21nii  359  pm5.18  362  biass  365  pm2.61ian  804  ecase3  953  4cases  961  elimh  968  pm4.42  972  3ecase  1379  ifpid  1441  ax6e  2095  exdistrf  2168  equvini  2180  dfsb2  2203  sbequi  2205  sbi1  2222  sbcom3  2241  sbco2  2245  sbco3  2247  sb9  2256  ax12vALT  2258  hbs1  2266  nfsb  2270  2ax6e  2280  sbal  2292  eujustALT  2303  pm2.61ine  2707  ralcom2  2923  eueq2  3180  moeq3  3183  mo2icl  3185  sbc2or  3244  sbcimdv  3297  unineq  3661  csb0  3739  sbcel12  3740  sbcne12  3743  sbcel2  3746  csbidm  3759  csbun  3766  csbin  3767  ralidm  3841  ifsb  3862  ifid  3886  ifnot  3894  ifan  3895  ifor  3896  csbif  3899  elimhyp  3907  elimhyp2v  3908  elimhyp3v  3909  elimhyp4v  3910  elimdhyp  3912  keephyp2v  3914  keephyp3v  3915  eqoreldif  3981  rabsnif  4010  tppreqb  4082  ssunsn2  4100  elpreqprlem  4130  dfopif  4133  csbuni  4196  sbcbr123  4426  sbcbr  4427  unisn2  4511  intabs  4537  class2set  4543  snexALT  4562  dtru  4567  dtruALT  4605  snex  4614  dtruALT2  4617  copsexg  4660  otsndisj  4679  otiunsndisj  4680  csbopab  4706  dfid3  4728  csbxp  4894  csbres  5086  csbima12  5163  soirri  5204  csbrn  5276  dmsnopss  5287  dmsnsnsn  5293  opswap  5302  unixpid  5350  nsuceq0  5482  ordsssuc2  5490  iotassuni  5541  iotaex  5542  dfiota4  5553  csbiota  5554  dffv3  5844  fvrn0  5870  ndmfv  5872  fveqres  5882  csbfv12  5883  csbfv  5885  dffv2  5922  fvco4i  5927  fvmptss  5942  fvmptex  5944  fvmptss2  5953  f0cli  6017  fvunsn  6081  fconst5  6107  csbriota  6250  riotassuni  6274  csbov123  6310  csbov  6311  0neqopab  6322  brfvopab  6324  elimdelov  6360  ovif12  6363  ndmovcl  6442  ndmovord  6447  elovmpt3imp  6512  difsnexi  6587  ordsuc  6629  ordsucelsuc  6637  1stval  6783  2ndval  6784  1st2val  6807  2nd2val  6808  bropopvvv  6862  bropfvvvvlem  6863  bropfvvvv  6864  suppimacnv  6913  suppssdm  6915  ressuppss  6922  suppun  6923  extmptsuppeq  6927  funsssuppss  6929  fczsupp0  6932  suppss  6933  suppssov1  6935  suppss2  6937  suppssfv  6939  supp0cosupp0  6942  imacosupp  6943  mpt2xopynvov0  6952  mpt2xopoveqd  6955  pwuninel  7009  smofvon2  7062  om0x  7208  brdomg  7566  snfi  7637  sdomirr  7696  domunsn  7709  2pwuninel  7714  snnen2o  7748  suppeqfsuppbi  7884  fsuppun  7889  funsnfsupp  7894  fipwuni  7927  oicl  8031  oif  8032  wemapso2  8055  card2on  8056  en2lp  8105  tctr  8211  r1tr  8234  rankdmr1  8259  r1pw  8303  r1pwALT  8304  rankuni  8321  scottex  8343  cardidm  8380  alephcard  8488  alephnbtwn  8489  cdacomen  8598  cfub  8666  cardcf  8669  cflecard  8670  cfle  8671  cflim2  8680  cfidm  8692  isf32lem9  8778  itunisuc  8836  itunitc1  8837  itunitc  8838  ituniiun  8839  axcc2lem  8853  alephreg  8994  pwcfsdom  8995  cfpwsdom  8996  axunndlem1  9007  axpownd  9013  tskmcl  9253  addcompi  9306  addasspi  9307  mulcompi  9308  mulasspi  9309  distrpi  9310  addnidpi  9313  nlt1pi  9318  addcompq  9362  addcomnq  9363  mulcompq  9364  mulcomnq  9365  adderpq  9368  mulerpq  9369  addassnq  9370  mulassnq  9371  distrnq  9373  genpass  9421  addcompr  9433  mulcompr  9435  distrpr  9440  ltexprlem7  9454  addcomsr  9498  addasssr  9499  mulcomsr  9500  mulasssr  9501  distrsr  9502  uzssz  11168  uzwo  11212  nn01to3  11247  elixx3g  11638  iooid  11654  elfz2  11782  injresinjlem  12018  injresinj  12019  fleqceilz  12075  modifeq2int  12146  ltweuz  12169  fzofi  12181  fsuppmapnn0fiubex  12198  hashrabrsn  12545  hashrabsn01  12546  hashrabsn1  12547  elprchashprn2  12567  hashss  12580  hashsnlei  12587  hash1snb  12588  hashgt12el  12590  hashgt12el2  12591  hash2pwpr  12630  hashge2el2dif  12632  ccatsymb  12725  swrd00  12773  swrd0  12789  swrdccatin1  12838  repswswrd  12886  0csh0  12894  cshwcl  12899  cshwidxmod  12904  repswcshw  12910  cshw1  12920  xptrrel  13055  trclfvcotrg  13091  relexpfld  13123  modfsummods  13864  gcdaddmlem  14503  pcmptcl  14847  prmgaplem5  15036  prmgaplem6  15037  cshwshash  15086  strfvss  15150  strfvi  15174  setsnid  15176  ressbas  15190  ressbasss  15192  resslem  15193  ress0  15194  ressress  15198  strle1  15232  0rest  15339  firest  15342  topnval  15344  xpsaddlem  15492  xpsvsca  15496  homffval  15606  comfffval  15614  oppchomfval  15630  oppcbas  15634  fullfunc  15822  fthfunc  15823  natfval  15862  fucbas  15876  fuchom  15877  arwval  15949  coafval  15970  xpcbas  16074  xpchomfval  16075  xpccofval  16078  lubfun  16237  glbfun  16250  oduval  16387  oduleval  16388  odumeet  16397  odujoin  16399  ipopos  16417  plusffval  16504  grpidval  16514  gsum0  16532  frmdplusg  16649  frmd0  16655  mgm2nsgrplem2  16664  mgm2nsgrplem3  16665  sgrp2rid2  16671  grpinvfval  16715  grpinvfvi  16718  grpsubfval  16719  mulgfval  16770  mulgfvi  16773  cntrval  16984  oppgval  17009  oppgplusfval  17010  symgbas  17032  symgplusg  17041  psgnfval  17152  odfval  17190  odfvalOLD  17193  oppglsm  17305  efgval  17378  mgpval  17737  mgpplusg  17738  ringidval  17748  opprval  17863  opprmulfval  17864  dvdsrval  17884  invrfval  17912  dvrfval  17923  staffval  18086  scaffval  18120  rlmval  18425  rlmsca2  18435  2idlval  18468  rrgval  18522  asclfval  18569  psrplusg  18616  psrmulr  18619  psrvscafval  18625  mplval  18663  mplcoe3  18701  evlval  18758  psr1val  18790  vr1val  18796  ply1val  18798  ply1basfvi  18845  ply1plusgfvi  18846  psr1sca2  18855  ply1sca2  18858  ply1ascl  18862  cply1mul  18898  gsummoncoe1  18909  evl1fval  18927  evl1fval1  18930  zrhval  19090  zlmlem  19099  zlmvsca  19104  chrval  19107  evpmss  19165  psgndiflemB  19179  ipffval  19226  thlbas  19270  thlle  19271  thloc  19273  pjfval  19280  dsmmval2  19310  mamufacex  19425  mavmulsolcl  19587  marrepfval  19596  marepvfval  19601  submafval  19615  mdetfval  19622  mdetfval1  19626  mdetunilem7  19654  mdetunilem8  19655  madufval  19673  minmar1fval  19682  mp2pm2mplem4  19844  tgdif0  20019  indislem  20026  resstopn  20213  iocpnfordt  20242  icomnfordt  20243  hmeofval  20784  ussval  21285  nmfval  21614  nghmfval  21738  nghmfvalOLD  21756  pcofval  22052  tchval  22203  ioombl  22530  ibladdlem  22789  itgaddlem1  22792  iblabs  22798  dvbsss  22869  perfdvf  22870  mdegfval  23023  deg1fval  23041  deg1fvi  23046  uc1pval  23102  mon1pval  23104  ttglem  24918  axcontlem12  25017  usgraedgprv  25115  usgra1v  25129  nbusgra  25168  nbgra0nb  25169  nbgranself2  25176  cusgra1v  25201  uvtxisvtx  25230  uvtx0  25231  uvtx01vtx  25232  1conngra  25415  wwlknfi  25478  wlk0  25501  clwwlkprop  25510  clwwlkgt0  25511  clwwlknprop  25512  clwlkisclwwlklem2a4  25524  2wlkonot3v  25615  2spthonot3v  25616  vdgrf  25638  nbhashuvtx1  25655  frgra2v  25739  1to2vfriswmgra  25746  2pthfrgra  25751  frgrancvvdeqlem2  25771  2spotdisj  25801  2spotiundisj  25802  2spotmdisj  25808  frgrareggt1  25856  frgrareg  25857  frgraregord013  25858  frgraogt3nreg  25860  friendship  25862  avril1  25912  ismgmOLD  26060  vafval  26234  bafval  26235  smfval  26236  vsfval  26266  bcsiALT  26844  resvsca  28600  resvlem  28601  cntnevol  29057  signsw0glem  29448  bnj1189  29824  mvtval  30144  mexval  30146  mexval2  30147  mdvval  30148  mrsubfval  30152  mrsubrn  30157  msubfval  30168  elmsubrn  30172  msubrn  30173  mvhfval  30177  mpstval  30179  msrfval  30181  mstaval  30188  mppsval  30216  mthmval  30219  dfrdg3  30449  trpredlem1  30474  bdayelon  30575  fvsingle  30693  unisnif  30698  funpartfv  30718  fullfunfv  30720  linedegen  30916  bj-elimhyp  31155  bj-ax6e  31268  bj-ax12v  31381  bj-hbs1  31384  bj-dtru  31414  bj-nfcsym  31496  bj-inftyexpidisj  31654  csbdif  31728  finxpreclem4  31788  finxp00  31796  wl-nfs1t  31873  wl-ax12  31915  wl-sbcom3  31927  itg2addnclem  31995  ibladdnclem  32000  itgaddnclem1  32002  iblabsnc  32008  iblmulc2nc  32009  ftc1anclem8  32026  tsbi1  32377  tsbi2  32378  ac6s6  32417  ax12  32477  equid1  32480  equid1ALT  32498  dvelimf-o  32502  ax12inda2ALT  32519  ax12inda2  32520  mzpmfp  35591  itgocn  36032  mendbas  36052  mendplusgfval  36053  mendmulrfval  36055  mendsca  36057  mendvscafval  36058  arearect  36102  areaquad  36103  addcomgi  36810  ax6e2ndeq  36927  2sb5ndVD  37304  2sb5ndALT  37326  sqwvfoura  38149  sqwvfourb  38150  fourierswlem  38151  fouriersw  38152  hspdifhsp  38501  hspmbllem2  38512  hspmbl  38514  tz6.12-afv  38766  ndmaovcl  38796  nltle2tri  38807  fzopredsuc  38811  iccpartiltu  38827  iccpartigtl  38828  iccpartlt  38829  icceuelpartlem  38840  iccpartnel  38843  evenprm2  38933  stgoldbwt  38968  pfx00  39018  pfx0  39019  n0snor2el  39089  otiunsndisjX  39098  xnn0xaddcl  39184  usgr1v  39432  nbuhgr  39513  nbumgr  39517  uhgrnbgr0nb  39524  nbgr1vtx  39528  nbgrnself2  39533  nbusgrvtxm1  39555  uvtxa0  39568  sizusglecusg  39626  wlkbProp  39732  rel1wlk  39741  1wlkvtxeledg  39773  lfgrwlkprop  39774  1conngr  39987  nzerooringczr  40399  pgrpgt2nabl  40476  suppmptcfin  40489  linc1  40543  lindslinindsimp2lem5  40580