Theorem pm2.61d1 164

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 163	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  166  pm2.61nii  171  pm2.01d  174  moexex  2380  2mo  2390  mosubopt  4712  predpoirr  5426  predfrirr  5427  funfv  5954  dffv2  5960  fvmptnf  5989  rdgsucmptnf  7172  frsucmptn  7181  mapdom2  7768  frfi  7841  oiexg  8075  wemapwe  8227  r1tr  8272  alephsing  8731  uzin  11219  sumrblem  13825  fsumcvg  13826  summolem2a  13829  fsumcvg2  13841  prodeq2ii  14015  prodrblem  14031  fprodcvg  14032  prodmolem2a  14036  zprod  14039  ptpjpre1  20634  qtopres  20761  fgabs  20942  ptcmplem3  21117  setsmstopn  21541  tngtopn  21706  cnmpt2pc  22004  pcoval2  22095  pcopt  22101  pcopt2  22102  itgle  22815  ibladdlem  22825  iblabslem  22833  iblabs  22834  iblabsr  22835  iblmulc2  22836  ditgneg  22860  nbgra0nb  25205  n4cyclfrgra  25794  poimirlem26  32010  poimirlem32  32016  ovoliunnfl  32026  voliunnfl  32028  volsupnfl  32029  itg2addnclem  32037  itg2gt0cn  32041  ibladdnclem  32042  iblabsnclem  32049  iblabsnc  32050  iblmulc2nc  32051  bddiblnc  32056  ftc1anclem7  32067  ftc1anclem8  32068  ftc1anc  32069  dicvalrelN  34797  dihvalrel  34891  fundmge2nop  39067  fun2dmnop  39068  umgr2adedgspth  39896  ldepspr  40538