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  moOLD  2305  moexex  2349  2mo  2360  2moOLD  2361  2moOLDOLD  2362  mosubopt  4604  funfv  5773  dffv2  5779  fvmptnf  5806  rdgsucmptnf  6900  frsucmptn  6909  mapdom2  7497  frfi  7572  oiexg  7764  wemapwe  7943  wemapweOLD  7944  r1tr  7998  alephsing  8460  uzin  10908  sumeq2ii  13185  sumrblem  13203  fsumcvg  13204  summolem2a  13207  fsumcvg2  13219  ptpjpre1  19159  qtopres  19286  fgabs  19467  ptcmplem3  19641  setsmstopn  20068  tngtopn  20251  cnmpt2pc  20515  pcoval2  20603  pcopt  20609  pcopt2  20610  itgle  21302  ibladdlem  21312  iblabslem  21320  iblabs  21321  iblabsr  21322  iblmulc2  21323  ditgneg  21347  nbgra0nb  23355  prodeq2ii  27441  prodrblem  27457  fprodcvg  27458  prodmolem2a  27462  zprod  27465  predpoirr  27673  predfrirr  27674  ovoliunnfl  28452  voliunnfl  28454  volsupnfl  28455  itg2addnclem  28462  itg2gt0cn  28466  ibladdnclem  28467  iblabsnclem  28474  iblabsnc  28475  iblmulc2nc  28476  bddiblnc  28481  ftc1anclem7  28492  ftc1anclem8  28493  ftc1anc  28494  n4cyclfrgra  30629  ldepspr  31026  dicvalrelN  34849  dihvalrel  34943