Theorem pm2.61d2 160

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

Hypotheses

Ref	Expression
pm2.61d2.1
pm2.61d2.2

Assertion

Ref	Expression
pm2.61d2

Proof of Theorem pm2.61d2

Step	Hyp	Ref	Expression
1		pm2.61d2.2	. . 3
2	1	a1i 11	. 2
3		pm2.61d2.1	. 2
4	2, 3	pm2.61d 158	1

Syntax hints:  -.wn 3  ->wi 4

This theorem is referenced by:  pm2.61ii  165  jaoi  379  nfald2  2073  nfsbd  2186  2ax6elem  2193  sbal1  2204  sbal2  2205  nfabd2  2640  rgen2a  2884  relimasn  5365  nfriotad  6265  tfinds  6694  curry1val  6893  curry2val  6897  onfununi  7031  findcard2s  7781  xpfi  7811  fiint  7817  acndom  8453  dfac12k  8548  iundom2g  8936  axpowndlem3OLD  8997  nqereu  9328  ltapr  9444  xrmax1  11405  xrmin2  11408  max1ALT  11416  hasheq0  12433  swrdvalodm2  12664  swrdvalodm  12665  cshw1  12790  bezout  14180  ptbasfi  20082  filcon  20384  pcopt  21522  ioorinv  21985  itg1addlem2  22104  itg1addlem4  22106  itgss  22218  bddmulibl  22245  wlkdvspthlem  24609  mdsymlem6  27327  sumdmdlem2  27338  wl-equsb4  30005  wl-sbalnae  30012

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8