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  856  nfald2  2453  2ax6elem  2478  nfsbd  2530  sbal1  2536  nfabd2  2935  rgen2a  3379  posn  5785  frsn  5787  relimasn  6114  nfriotadw  7412  nfriotad  7416  tfinds  7897  curry1val  8146  curry2val  8150  onfununi  8397  findcard2s  9231  xpfiOLD  9387  prfi  9391  fiint  9394  fiintOLD  9395  acndom  10120  dfac12k  10217  iundom2g  10609  nqereu  10998  ltapr  11114  xrmax1  13237  xrmin2  13240  max1ALT  13248  hasheq0  14412  swrdnd2  14703  cshw1  14870  bezout  16590  ptbasfi  23610  filconn  23912  pcopt  25074  ioorinv  25630  itg1addlem2  25751  itg1addlem4  25753  itg1addlem4OLD  25754  itgss  25867  bddmulibl  25894  maxs1  27828  mins2  27831  pthdlem2  29804  mdsymlem6  32440  sumdmdlem2  32451  bj-ax6elem1  36632  wl-equsb4  37511  wl-sbalnae  37516  poimirlem13  37593  poimirlem25  37605  poimirlem27  37607  remullid  42409  sbgoldbaltlem1  47653  setrec2fun  48784