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  moexex  2360  2mo  2370  2moOLD  2371  mosubopt  4734  funfv  5915  dffv2  5921  fvmptnf  5949  rdgsucmptnf  7087  frsucmptn  7096  mapdom2  7681  frfi  7757  oiexg  7952  wemapwe  8130  wemapweOLD  8131  r1tr  8185  alephsing  8647  uzin  11114  sumrblem  13618  fsumcvg  13619  summolem2a  13622  fsumcvg2  13634  prodeq2ii  13805  prodrblem  13821  fprodcvg  13822  prodmolem2a  13826  zprod  13829  ptpjpre1  20241  qtopres  20368  fgabs  20549  ptcmplem3  20723  setsmstopn  21150  tngtopn  21333  cnmpt2pc  21597  pcoval2  21685  pcopt  21691  pcopt2  21692  itgle  22385  ibladdlem  22395  iblabslem  22403  iblabs  22404  iblabsr  22405  iblmulc2  22406  ditgneg  22430  nbgra0nb  24634  n4cyclfrgra  25223  predpoirr  29520  predfrirr  29521  ovoliunnfl  30299  voliunnfl  30301  volsupnfl  30302  itg2addnclem  30309  itg2gt0cn  30313  ibladdnclem  30314  iblabsnclem  30321  iblabsnc  30322  iblmulc2nc  30323  bddiblnc  30328  ftc1anclem7  30339  ftc1anclem8  30340  ftc1anc  30341  ldepspr  33347  dicvalrelN  37328  dihvalrel  37422