Theorem pm2.61d2 164

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 162	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  169  jaoi  381  nfald2  2167  nfsbd  2273  2ax6elem  2280  sbal1  2291  sbal2  2292  nfabd2  2613  rgen2a  2817  relimasn  5194  nfriotad  6265  tfinds  6691  curry1val  6894  curry2val  6898  onfununi  7065  findcard2s  7817  xpfi  7847  fiint  7853  acndom  8487  dfac12k  8582  iundom2g  8970  nqereu  9359  ltapr  9475  xrmax1  11477  xrmin2  11480  max1ALT  11488  hasheq0  12551  swrdnd2  12796  cshw1  12928  bezout  14522  ptbasfi  20608  filcon  20910  pcopt  22065  ioorinv  22540  ioorinvOLD  22545  itg1addlem2  22667  itg1addlem4  22669  itgss  22781  bddmulibl  22808  wlkdvspthlem  25349  mdsymlem6  28073  sumdmdlem2  28084  bj-ax6elem1  31276  wl-equsb4  31897  wl-sbalnae  31904  poimirlem13  31965  poimirlem25  31977  poimirlem27  31979  sgoldbaltlem1  38890