Theorem pm2.61d1 159

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 158	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  161  pm2.61nii  166  pm2.01d  169  moOLD  2327  moexex  2371  2mo  2382  2moOLD  2383  2moOLDOLD  2384  mosubopt  4745  funfv  5932  dffv2  5938  fvmptnf  5965  rdgsucmptnf  7092  frsucmptn  7101  mapdom2  7685  frfi  7761  oiexg  7956  wemapwe  8135  wemapweOLD  8136  r1tr  8190  alephsing  8652  uzin  11110  sumeq2ii  13474  sumrblem  13492  fsumcvg  13493  summolem2a  13496  fsumcvg2  13508  ptpjpre1  19807  qtopres  19934  fgabs  20115  ptcmplem3  20289  setsmstopn  20716  tngtopn  20899  cnmpt2pc  21163  pcoval2  21251  pcopt  21257  pcopt2  21258  itgle  21951  ibladdlem  21961  iblabslem  21969  iblabs  21970  iblabsr  21971  iblmulc2  21972  ditgneg  21996  nbgra0nb  24105  n4cyclfrgra  24694  prodeq2ii  28622  prodrblem  28638  fprodcvg  28639  prodmolem2a  28643  zprod  28646  predpoirr  28854  predfrirr  28855  ovoliunnfl  29633  voliunnfl  29635  volsupnfl  29636  itg2addnclem  29643  itg2gt0cn  29647  ibladdnclem  29648  iblabsnclem  29655  iblabsnc  29656  iblmulc2nc  29657  bddiblnc  29662  ftc1anclem7  29673  ftc1anclem8  29674  ftc1anc  29675  ldepspr  32147  dicvalrelN  35982  dihvalrel  36076