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  854  nfald2  2447  2ax6elem  2472  nfsbd  2528  sbal1  2535  nfabd2  2935  rgen2a  3158  posn  5673  frsn  5675  relimasn  5991  nfriotadw  7236  nfriotad  7240  tfinds  7700  curry1val  7936  curry2val  7940  onfununi  8163  findcard2s  8930  xpfi  9063  fiint  9069  acndom  9808  dfac12k  9904  iundom2g  10297  nqereu  10686  ltapr  10802  xrmax1  12908  xrmin2  12911  max1ALT  12919  hasheq0  14076  swrdnd2  14366  cshw1  14533  bezout  16249  ptbasfi  22730  filconn  23032  pcopt  24183  ioorinv  24738  itg1addlem2  24859  itg1addlem4  24861  itg1addlem4OLD  24862  itgss  24974  bddmulibl  25001  pthdlem2  28132  mdsymlem6  30766  sumdmdlem2  30777  bj-ax6elem1  34843  wl-equsb4  35708  wl-sbalnae  35713  poimirlem13  35786  poimirlem25  35798  poimirlem27  35800  remulid2  40412  sbgoldbaltlem1  45200  setrec2fun  46367