Theorem pm2.61d2 181

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 179	1 ⊢ (𝜑 → 𝜒)

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  183  jaoi  858  nfald2  2449  2ax6elem  2474  nfsbd  2526  sbal1  2532  nfabd2  2922  rgen2a  3333  posn  5717  frsn  5719  relimasn  6050  nfriotadw  7332  nfriotad  7335  tfinds  7811  curry1val  8055  curry2val  8059  onfununi  8281  findcard2s  9100  prfi  9234  fiint  9237  acndom  9973  dfac12k  10070  iundom2g  10462  nqereu  10852  ltapr  10968  xrmax1  13127  xrmin2  13130  max1ALT  13138  hasheq0  14325  swrdnd2  14618  cshw1  14784  bezout  16512  ptbasfi  23546  filconn  23848  pcopt  24989  ioorinv  25543  itg1addlem2  25664  itg1addlem4  25666  itgss  25779  bddmulibl  25806  maxs1  27733  mins2  27736  pthdlem2  29836  mdsymlem6  32479  sumdmdlem2  32490  bj-ax6elem1  36960  wl-equsb4  37882  wl-sbalnae  37887  poimirlem13  37954  poimirlem25  37966  poimirlem27  37968  remullid  42866  sbgoldbaltlem1  48255  setrec2fun  50167