Theorem pm2.61d1 171

Description: Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)

Hypotheses

Ref	Expression
pm2.61d1.1	|- ( ph -> ( ps -> ch ) )
pm2.61d1.2	|- ( -. ps -> ch )

Assertion

Ref	Expression
pm2.61d1	|- ( ph -> ch )

Proof of Theorem pm2.61d1

Step	Hyp	Ref	Expression
1		pm2.61d1.1	. 2 |- ( ph -> ( ps -> ch ) )
2		pm2.61d1.2	. . 3 |- ( -. ps -> ch )
3	2	a1i 11	. 2 |- ( ph -> ( -. ps -> ch ) )
4	1, 3	pm2.61d 170	1 |- ( ph -> ch )

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:  ja  173  pm2.61nii  178  pm2.01d  181  moexex  2541  2mo  2551  mosubopt  4972  predpoirr  5708  predfrirr  5709  funfv  6265  dffv2  6271  fvmptnf  6302  rdgsucmptnf  7525  frsucmptn  7534  mapdom2  8131  frfi  8205  oiexg  8440  wemapwe  8594  r1tr  8639  alephsing  9098  uzin  11720  fundmge2nop0  13274  fun2dmnop0  13276  sumrblem  14442  fsumcvg  14443  summolem2a  14446  fsumcvg2  14458  prodeq2ii  14643  prodrblem  14659  fprodcvg  14660  prodmolem2a  14664  zprod  14667  ptpjpre1  21374  qtopres  21501  fgabs  21683  ptcmplem3  21858  setsmstopn  22283  tngtopn  22454  cnmpt2pc  22727  pcoval2  22816  pcopt  22822  pcopt2  22823  itgle  23576  ibladdlem  23586  iblabslem  23594  iblabs  23595  iblabsr  23596  iblmulc2  23597  ditgneg  23621  umgr2adedgspth  26844  n4cyclfrgr  27155  poimirlem26  33435  poimirlem32  33441  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  itg2addnclem  33461  itg2gt0cn  33465  ibladdnclem  33466  iblabsnclem  33473  iblabsnc  33474  iblmulc2nc  33475  bddiblnc  33480  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  dicvalrelN  36474  dihvalrel  36568  ldepspr  42262