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  2moOLD  2352  mosubopt  4719  predpoirr  5427  predfrirr  5428  funfv  5948  dffv2  5954  fvmptnf  5983  rdgsucmptnf  7155  frsucmptn  7164  mapdom2  7749  frfi  7822  oiexg  8050  wemapwe  8201  r1tr  8246  alephsing  8704  uzin  11191  sumrblem  13755  fsumcvg  13756  summolem2a  13759  fsumcvg2  13771  prodeq2ii  13945  prodrblem  13961  fprodcvg  13962  prodmolem2a  13966  zprod  13969  ptpjpre1  20517  qtopres  20644  fgabs  20825  ptcmplem3  21000  setsmstopn  21424  tngtopn  21589  cnmpt2pc  21852  pcoval2  21940  pcopt  21946  pcopt2  21947  itgle  22644  ibladdlem  22654  iblabslem  22662  iblabs  22663  iblabsr  22664  iblmulc2  22665  ditgneg  22689  nbgra0nb  25002  n4cyclfrgra  25591  poimirlem26  31670  poimirlem32  31676  ovoliunnfl  31686  voliunnfl  31688  volsupnfl  31689  itg2addnclem  31697  itg2gt0cn  31701  ibladdnclem  31702  iblabsnclem  31709  iblabsnc  31710  iblmulc2nc  31711  bddiblnc  31716  ftc1anclem7  31727  ftc1anclem8  31728  ftc1anc  31729  dicvalrelN  34462  dihvalrel  34556  ldepspr  39026