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  2046  nfsbd  2170  2ax6elem  2179  sbal1  2193  sbal2  2195  nfabd2  2650  rgen2a  2891  relimasn  5358  nfriotad  6251  tfinds  6672  curry1val  6873  curry2val  6877  onfununi  7009  findcard2s  7757  xpfi  7787  fiint  7793  acndom  8428  dfac12k  8523  iundom2g  8911  axpowndlem3OLD  8972  nqereu  9303  ltapr  9419  xrmax1  11372  xrmin2  11375  max1ALT  11383  hasheq0  12395  swrdvalodm2  12621  swrdvalodm  12622  cshw1  12747  bezout  14032  ptbasfi  19814  filcon  20116  pcopt  21254  ioorinv  21717  itg1addlem2  21836  itg1addlem4  21838  itgss  21950  bddmulibl  21977  wlkdvspthlem  24282  mdsymlem6  27000  sumdmdlem2  27011  wl-equsb4  29579  wl-sbalnae  29586