Theorem pm2.61d2 182

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 180	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  184  jaoi  863  nfald2  2453  2ax6elem  2478  nfsbd  2530  sbal1  2536  nfabd2  2925  rgen2a  3336  posn  5711  frsn  5713  relimasn  6044  nfriotadw  7328  nfriotad  7331  tfinds  7807  curry1val  8051  curry2val  8055  onfununi  8278  findcard2s  9097  prfi  9231  fiint  9234  acndom  9971  dfac12k  10068  iundom2g  10460  nqereu  10850  ltapr  10966  xrmax1  13125  xrmin2  13128  max1ALT  13136  hasheq0  14323  swrdnd2  14616  cshw1  14782  bezout  16510  ptbasfi  23571  filconn  23873  pcopt  25014  ioorinv  25568  itg1addlem2  25689  itg1addlem4  25691  itgss  25804  bddmulibl  25831  maxs1  27758  mins2  27761  pthdlem2  29861  mdsymlem6  32504  sumdmdlem2  32515  bj-ax6elem1  37013  wl-equsb4  37935  wl-sbalnae  37940  poimirlem13  38007  poimirlem25  38019  poimirlem27  38021  remullid  42918  sbgoldbaltlem1  48277  setrec2fun  50189