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  2129  nfsbd  2238  2ax6elem  2245  sbal1  2256  sbal2  2257  nfabd2  2606  rgen2a  2853  relimasn  5208  nfriotad  6273  tfinds  6698  curry1val  6898  curry2val  6902  onfununi  7066  findcard2s  7816  xpfi  7846  fiint  7852  acndom  8484  dfac12k  8579  iundom2g  8967  nqereu  9356  ltapr  9472  xrmax1  11472  xrmin2  11475  max1ALT  11483  hasheq0  12545  swrdnd2  12785  cshw1  12917  bezout  14503  ptbasfi  20588  filcon  20890  pcopt  22045  ioorinv  22520  ioorinvOLD  22525  itg1addlem2  22647  itg1addlem4  22649  itgss  22761  bddmulibl  22788  wlkdvspthlem  25329  mdsymlem6  28053  sumdmdlem2  28064  wl-equsb4  31843  wl-sbalnae  31850  poimirlem13  31911  poimirlem25  31923  poimirlem27  31925  sgoldbaltlem1  38636