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  788  ecase3  932  4cases  940  elimh  947  pm4.42  951  3ecase  1323  ax6e  1946  exdistrf  2025  equvini  2037  dfsb2  2064  sbequi  2066  sbnOLD  2083  sbi1  2084  sbcom3  2105  sbco2  2111  sbco2OLD  2112  sbco3  2114  sbco3OLD  2115  sb9  2126  sb9iOLD  2128  ax12v  2130  hbs1  2141  nfsb  2146  2ax6e  2158  sbal1OLD  2172  sbal  2174  sbalOLD  2175  ax12  2205  equid1  2208  equid1ALT  2226  dvelimf-o  2230  ax12inda2ALT  2247  ax12inda2  2248  eujustALT  2256  moexexOLD  2350  pm2.61ne  2686  pm2.61ine  2687  rgen2a  2782  ralcom2  2885  eueq2  3133  moeq3  3136  mo2icl  3138  sbc2or  3195  sbcimdv  3255  unineq  3600  csb0  3674  sbcel12  3675  sbcne12  3679  sbcel2  3683  csbidm  3698  csbun  3709  csbin  3712  ralidm  3783  ifsb  3802  ifid  3826  ifnot  3834  ifan  3835  ifor  3836  csbif  3839  elimhyp  3848  elimhyp2v  3849  elimhyp3v  3850  elimhyp4v  3851  elimdhyp  3853  keephyp2v  3855  keephyp3v  3856  rabsnif  3944  tppreqb  4014  ssunsn2  4032  dfopif  4056  csbuni  4119  sbcbr123  4343  sbcbr  4345  unisn2  4428  intabs  4453  class2set  4459  snexALT  4478  dtru  4483  dtruALT  4524  snex  4533  dtruALT2  4536  copsexg  4576  copsexgOLD  4577  csbopab  4620  dfid3  4637  nsuceq0  4799  ordsssuc2  4807  csbxp  4918  csbres  5113  csbima12  5186  soirri  5224  soirriOLD  5229  csbrn  5299  dmsnopss  5311  dmsnsnsn  5317  opswap  5326  unixpid  5372  iotassuni  5397  iotaex  5398  dfiota4  5409  csbiota  5410  dffv3  5687  fvrn0  5712  ndmfv  5714  fveqres  5724  csbfv12  5725  csbfv  5728  dffv2  5764  fvco4i  5769  fvmptss  5782  fvmptex  5784  fvmptss2  5793  f0cli  5854  fvunsn  5910  fconst5  5935  csbriota  6064  riotassuniOLD  6089  csbov123  6122  csbov  6123  0neqopab  6131  elimdelov  6167  ovif12  6170  ndmovcl  6248  ndmovord  6253  difsnexi  6384  ordsuc  6425  ordsucelsuc  6433  1stval  6579  2ndval  6580  1st2val  6602  2nd2val  6603  bropopvvv  6653  suppimacnv  6701  suppssdm  6703  ressuppss  6708  suppun  6709  extmptsuppeq  6713  funsssuppss  6715  fczsupp0  6718  suppss  6719  suppssov1  6721  suppss2  6723  suppssfv  6725  supp0cosupp0  6728  imacosupp  6729  mpt2xopynvov0  6735  mpt2xopoveqd  6738  pwuninel  6794  smofvon2  6817  om0x  6959  brdomg  7320  snfi  7390  sdomirr  7448  domunsn  7461  2pwuninel  7466  suppeqfsuppbi  7634  fsuppun  7639  funsnfsupp  7644  fipwuni  7676  oicl  7743  oif  7744  wemapso2  7768  card2on  7769  en2lp  7819  tctr  7960  r1tr  7983  rankdmr1  8008  r1pw  8052  r1pwOLD  8053  rankuni  8070  scottex  8092  cardidm  8129  alephcard  8240  alephnbtwn  8241  cdacomen  8350  cfub  8418  cardcf  8421  cflecard  8422  cfle  8423  cflim2  8432  cfidm  8444  isf32lem9  8530  itunisuc  8588  itunitc1  8589  itunitc  8590  ituniiun  8591  axcc2lem  8605  alephreg  8746  pwcfsdom  8747  cfpwsdom  8748  axunndlem1  8759  axpownd  8767  tskmcl  9008  addcompi  9063  addasspi  9064  mulcompi  9065  mulasspi  9066  distrpi  9067  addnidpi  9070  nlt1pi  9075  addcompq  9119  addcomnq  9120  mulcompq  9121  mulcomnq  9122  adderpq  9125  mulerpq  9126  addassnq  9127  mulassnq  9128  distrnq  9130  genpass  9178  addcompr  9190  mulcompr  9192  distrpr  9197  ltexprlem7  9211  addcomsr  9254  addasssr  9255  mulcomsr  9256  mulasssr  9257  distrsr  9258  uzssz  10880  uzwo  10917  uzwoOLD  10918  elixx3g  11313  iooid  11328  elfz2  11444  injresinjlem  11638  injresinj  11639  fleqceilz  11693  modifeq2int  11761  ltweuz  11784  fzofi  11796  hashrabrsn  12137  elprchashprn2  12156  hashss  12166  hashsnlei  12170  hash1snb  12171  euhash1  12172  hashgt12el  12173  hashgt12el2  12174  hash2pwpr  12182  hashge2el2dif  12184  ccatsymb  12281  swrd00  12314  swrdnd  12326  swrd0  12327  swrdccatin1  12374  repswswrd  12422  0csh0  12430  cshwcl  12435  cshwidxmod  12440  repswcshw  12446  cshw1  12456  gcdaddmlem  13712  pcmptcl  13953  cshwshash  14131  strfvss  14192  strfvi  14214  setsnid  14216  ressbas  14228  ressbasss  14230  resslem  14231  ress0  14232  ressress  14235  strle1  14269  0rest  14368  firest  14371  topnval  14373  xpsaddlem  14513  xpsvsca  14517  homffval  14630  comfffval  14637  oppchomfval  14653  oppcbas  14657  fullfunc  14816  fthfunc  14817  natfval  14856  fucbas  14870  fuchom  14871  arwval  14911  coafval  14932  xpcbas  14988  xpchomfval  14989  xpccofval  14992  lubfun  15150  glbfun  15163  oduval  15300  oduleval  15301  odumeet  15310  odujoin  15312  ipopos  15330  plusffval  15427  grpidval  15432  gsum0  15510  frmdplusg  15532  frmd0  15538  grpinvfval  15576  grpinvfvi  15579  grpsubfval  15580  mulgfval  15628  mulgfvi  15631  cntrval  15837  oppgval  15862  oppgplusfval  15863  symgbas  15885  symgplusg  15894  psgnfval  16006  odfval  16036  oppglsm  16141  efgval  16214  mgpval  16594  mgpplusg  16595  rngidval  16605  opprval  16716  opprmulfval  16717  dvdsrval  16737  invrfval  16765  dvrfval  16776  staffval  16932  scaffval  16966  rlmval  17272  rlmsca2  17282  2idlval  17315  rrgval  17358  asclfval  17405  psrplusg  17452  psrmulr  17455  psrvscafval  17461  mplval  17501  mplcoe3  17545  mplcoe3OLD  17546  evlval  17610  psr1val  17642  vr1val  17648  ply1val  17650  ply1basfvi  17696  ply1plusgfvi  17697  psr1sca2  17706  ply1sca2  17709  ply1ascl  17712  evl1fval  17762  evl1fval1  17765  zrhval  17939  zlmlem  17948  zlmvsca  17953  chrval  17956  evpmss  18016  psgndiflemB  18030  ipffval  18077  thlbas  18121  thlle  18122  thloc  18124  pjfval  18131  dsmmval2  18161  mamufacex  18289  mavmulsolcl  18362  marrepfval  18371  marepvfval  18376  submafval  18390  mdetfval  18397  mdetfval1  18401  mdetunilem7  18424  mdetunilem8  18425  madufval  18443  minmar1fval  18452  tgdif0  18597  indislem  18604  resstopn  18790  iocpnfordt  18819  icomnfordt  18820  hmeofval  19331  ussval  19834  nmfval  20181  nghmfval  20301  pcofval  20582  tchval  20733  ioombl  21046  ibladdlem  21297  itgaddlem1  21300  iblabs  21306  limccnp2  21367  dvbsss  21377  perfdvf  21378  mdegfval  21531  deg1fval  21551  deg1fvi  21556  uc1pval  21611  mon1pval  21613  ttglem  23122  axcontlem12  23221  usgraedgprv  23295  usgra1v  23308  nbusgra  23339  nbgra0nb  23340  nbgranself2  23347  cusgra1v  23369  uvtxisvtx  23398  uvtx0  23399  uvtx01vtx  23400  1conngra  23561  vdgrf  23568  avril1  23656  ismgm  23807  vafval  23981  bafval  23982  smfval  23983  vsfval  24013  bcsiALT  24581  resvsca  26298  resvlem  26299  cntnevol  26642  signsw0glem  26954  dfrdg3  27610  trpredlem1  27691  bdayelon  27821  fvsingle  27951  unisnif  27956  funpartfv  27976  fullfunfv  27978  linedegen  28174  wl-nfs1t  28367  wl-sbcom3  28411  itg2addnclem  28443  ibladdnclem  28448  itgaddnclem1  28450  iblabsnc  28456  iblmulc2nc  28457  ftc1anclem5  28471  ftc1anclem8  28474  tsim2  28942  tsim3  28943  tsbi1  28944  tsbi2  28945  tsbi3  28946  tsan2  28953  tsan3  28954  tsor2  28959  tsor3  28960  ac6s6  28984  mzpmfp  29083  mzpmfpOLD  29084  itgocn  29521  mendbas  29541  mendplusgfval  29542  mendmulrfval  29544  mendsca  29546  mendvscafval  29547  arearect  29591  areaquad  29592  addcomgi  29712  tz6.12-afv  30079  ndmaovcl  30109  otsndisj  30131  otiunsndisj  30132  otiunsndisjX  30133  elovmpt3imp  30160  nn01to3  30187  hashrabsn01  30232  hashrabsn1  30233  modfsummods  30244  wlk0  30292  wwlknfi  30370  2wlkonot3v  30394  2spthonot3v  30395  clwwlkprop  30433  clwwlkgt0  30434  clwwlknprop  30435  clwlkisclwwlklem2a4  30446  nbhashuvtx1  30533  frgra2v  30591  1to2vfriswmgra  30598  2pthfrgra  30603  frgrancvvdeqlem2  30624  2spotdisj  30654  2spotiundisj  30655  2spotmdisj  30661  frgrareggt1  30709  frgrareg  30710  frgraregord013  30711  frgraogt3nreg  30713  friendship  30715  snnen2o  30738  pgrpgt2nabel  30769  suppmptcfin  30793  fsuppmapnn0fiubex  30800  gsummoncoe1  30843  mp2pm2mplem4  30919  linc1  30959  lindslinindsimp2lem5  30996  ax6e2ndeq  31268  2sb5ndVD  31646  2sb5ndALT  31668  bnj1189  32000  bj-dfif5ALT  32086  bj-ifid  32091  bj-elimhyp  32096  bj-ax12v  32283  bj-hbs1  32287  bj-dtru  32318  bj-nfcsym  32395  bj-inftyexpidisj  32533