Theorem pm2.61d1 153

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 152	1 |- ( ph -> ch )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  ja  155  pm2.61nii  160  pm2.01d  163  ax10lem2OLD  1992  mo  2276  2mo  2332  mosubopt  4414  funfv  5749  dffv2  5755  fvmptnf  5781  rdgsucmptnf  6646  frsucmptn  6655  mapdom2  7237  frfi  7311  oiexg  7460  wemapwe  7610  r1tr  7658  alephsing  8112  uzin  10474  sumeq2ii  12442  sumrblem  12460  fsumcvg  12461  summolem2a  12464  zsum  12467  fsumcvg2  12476  ptpjpre1  17556  qtopres  17683  fgabs  17864  ptcmplem3  18038  setsmstopn  18461  tngtopn  18644  cnmpt2pc  18906  pcoval2  18994  pcopt  19000  pcopt2  19001  itgle  19654  ibladdlem  19664  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  ditgneg  19697  nbgra0nb  21394  prodeq2ii  25192  prodrblem  25208  fprodcvg  25209  prodmolem2a  25213  zprod  25216  predpoirr  25411  predfrirr  25412  wl-pm5.74lem  26131  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  itg2addnclem  26155  itg2gt0cn  26159  ibladdnclem  26160  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  bddiblnc  26174  n4cyclfrgra  28122  dicvalrelN  31668  dihvalrel  31762

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8