Theorem pm2.61d2 171

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 169	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  176  jaoi  393  nfald2  2319  nfsbd  2430  2ax6elem  2437  sbal1  2448  sbal2  2449  nfabd2  2770  rgen2a  2960  posn  5110  frsn  5112  relimasn  5407  nfriotad  6519  tfinds  6951  curry1val  7157  curry2val  7161  onfununi  7325  findcard2s  8086  xpfi  8116  fiint  8122  acndom  8757  dfac12k  8852  iundom2g  9241  nqereu  9630  ltapr  9746  xrmax1  11880  xrmin2  11883  max1ALT  11891  hasheq0  13015  swrdnd2  13285  cshw1  13419  bezout  15098  ptbasfi  21194  filcon  21497  pcopt  22630  ioorinv  23150  itg1addlem2  23270  itg1addlem4  23272  itgss  23384  bddmulibl  23411  wlkdvspthlem  26137  mdsymlem6  28651  sumdmdlem2  28662  bj-ax6elem1  31840  wl-equsb4  32517  wl-sbalnae  32524  poimirlem13  32592  poimirlem25  32604  poimirlem27  32606  sgoldbaltlem1  40201  pthdlem2  40974  setrec2fun  42238