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  857  nfald2  2449  2ax6elem  2474  nfsbd  2526  sbal1  2532  nfabd2  2928  rgen2a  3370  posn  5770  frsn  5772  relimasn  6102  nfriotadw  7397  nfriotad  7400  tfinds  7882  curry1val  8131  curry2val  8135  onfununi  8382  findcard2s  9206  xpfiOLD  9360  prfi  9364  fiint  9367  fiintOLD  9368  acndom  10092  dfac12k  10189  iundom2g  10581  nqereu  10970  ltapr  11086  xrmax1  13218  xrmin2  13221  max1ALT  13229  hasheq0  14403  swrdnd2  14694  cshw1  14861  bezout  16581  ptbasfi  23590  filconn  23892  pcopt  25056  ioorinv  25612  itg1addlem2  25733  itg1addlem4  25735  itgss  25848  bddmulibl  25875  maxs1  27811  mins2  27814  pthdlem2  29789  mdsymlem6  32428  sumdmdlem2  32439  bj-ax6elem1  36668  wl-equsb4  37559  wl-sbalnae  37564  poimirlem13  37641  poimirlem25  37653  poimirlem27  37655  remullid  42468  sbgoldbaltlem1  47771  setrec2fun  49266