Theorem pm2.61d1 162

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 161	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  164  pm2.61nii  169  pm2.01d  172  moexex  2341  2mo  2351  mosubopt  4654  predpoirr  5363  predfrirr  5364  funfv  5885  dffv2  5891  fvmptnf  5920  rdgsucmptnf  7095  frsucmptn  7104  mapdom2  7689  frfi  7762  oiexg  7996  wemapwe  8147  r1tr  8192  alephsing  8650  uzin  11135  sumrblem  13713  fsumcvg  13714  summolem2a  13717  fsumcvg2  13729  prodeq2ii  13903  prodrblem  13919  fprodcvg  13920  prodmolem2a  13924  zprod  13927  ptpjpre1  20521  qtopres  20648  fgabs  20829  ptcmplem3  21004  setsmstopn  21428  tngtopn  21593  cnmpt2pc  21891  pcoval2  21982  pcopt  21988  pcopt2  21989  itgle  22702  ibladdlem  22712  iblabslem  22720  iblabs  22721  iblabsr  22722  iblmulc2  22723  ditgneg  22747  nbgra0nb  25092  n4cyclfrgra  25681  poimirlem26  31867  poimirlem32  31873  ovoliunnfl  31883  voliunnfl  31885  volsupnfl  31886  itg2addnclem  31894  itg2gt0cn  31898  ibladdnclem  31899  iblabsnclem  31906  iblabsnc  31907  iblmulc2nc  31908  bddiblnc  31913  ftc1anclem7  31924  ftc1anclem8  31925  ftc1anc  31926  dicvalrelN  34659  dihvalrel  34753  fundmge2nop  38826  fun2dmnop  38827  ldepspr  39853