Theorem pm2.61d2 160

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 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:  pm2.61ii  165  jaoi  379  nfald2  2023  nfsbd  2148  2ax6elem  2157  sbal1  2171  sbal2  2173  nfabd2  2597  relimasn  5192  nfriotad  6060  tfinds  6470  curry1val  6665  curry2val  6669  onfununi  6802  findcard2s  7553  xpfi  7583  fiint  7588  acndom  8221  dfac12k  8316  iundom2g  8704  axpowndlem3OLD  8765  nqereu  9098  ltapr  9214  xrmax1  11147  xrmin2  11150  max1ALT  11158  hasheq0  12131  swrdvalodm2  12333  swrdvalodm  12334  cshw1  12456  bezout  13726  ptbasfi  19154  filcon  19456  pcopt  20594  ioorinv  21056  itg1addlem2  21175  itg1addlem4  21177  itgss  21289  bddmulibl  21316  wlkdvspthlem  23506  mdsymlem6  25812  sumdmdlem2  25823  wl-equsb4  28381  wl-sbalnae  28388