Theorem pm2.61d2 165

Description: Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.)

Hypotheses

Ref	Expression
pm2.61d2.1	|- ( ph -> ( -. ps -> ch ) )
pm2.61d2.2	|- ( ps -> ch )

Assertion

Ref	Expression
pm2.61d2	|- ( ph -> ch )

Proof of Theorem pm2.61d2

Step	Hyp	Ref	Expression
1		pm2.61d2.2	. . 3 |- ( ps -> ch )
2	1	a1i 11	. 2 |- ( ph -> ( ps -> ch ) )
3		pm2.61d2.1	. 2 |- ( ph -> ( -. ps -> ch ) )
4	2, 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:  pm2.61ii  170  jaoi  386  nfald2  2180  nfsbd  2291  2ax6elem  2298  sbal1  2309  sbal2  2310  nfabd2  2631  rgen2a  2820  relimasn  5197  nfriotad  6278  tfinds  6705  curry1val  6908  curry2val  6912  onfununi  7078  findcard2s  7830  xpfi  7860  fiint  7866  acndom  8500  dfac12k  8595  iundom2g  8983  nqereu  9372  ltapr  9488  xrmax1  11493  xrmin2  11496  max1ALT  11504  hasheq0  12582  swrdnd2  12843  cshw1  12978  bezout  14589  ptbasfi  20673  filcon  20976  pcopt  22131  ioorinv  22607  ioorinvOLD  22612  itg1addlem2  22734  itg1addlem4  22736  itgss  22848  bddmulibl  22875  wlkdvspthlem  25416  mdsymlem6  28142  sumdmdlem2  28153  bj-ax6elem1  31328  wl-equsb4  31955  wl-sbalnae  31962  poimirlem13  32017  poimirlem25  32029  poimirlem27  32031  sgoldbaltlem1  39025  pthdlem2  39954