Theorem pm2.61d2 172

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 170	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  177  jaoi  394  nfald2  2331  nfsbd  2442  2ax6elem  2449  sbal1  2460  sbal2  2461  nfabd2  2784  rgen2a  2977  posn  5187  frsn  5189  relimasn  5488  nfriotad  6619  tfinds  7059  curry1val  7270  curry2val  7274  onfununi  7438  findcard2s  8201  xpfi  8231  fiint  8237  acndom  8874  dfac12k  8969  iundom2g  9362  nqereu  9751  ltapr  9867  xrmax1  12006  xrmin2  12009  max1ALT  12017  hasheq0  13154  swrdnd2  13433  cshw1  13568  bezout  15260  ptbasfi  21384  filconn  21687  pcopt  22822  ioorinv  23344  itg1addlem2  23464  itg1addlem4  23466  itgss  23578  bddmulibl  23605  pthdlem2  26664  mdsymlem6  29267  sumdmdlem2  29278  bj-ax6elem1  32651  wl-equsb4  33338  wl-sbalnae  33345  poimirlem13  33422  poimirlem25  33434  poimirlem27  33436  sbgoldbaltlem1  41667  setrec2fun  42439