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  855  nfald2  2444  2ax6elem  2469  nfsbd  2521  sbal1  2527  nfabd2  2929  rgen2a  3367  posn  5761  frsn  5763  relimasn  6083  nfriotadw  7375  nfriotad  7379  tfinds  7851  curry1val  8093  curry2val  8097  onfununi  8343  findcard2s  9167  xpfiOLD  9320  fiint  9326  acndom  10048  dfac12k  10144  iundom2g  10537  nqereu  10926  ltapr  11042  xrmax1  13156  xrmin2  13159  max1ALT  13167  hasheq0  14325  swrdnd2  14607  cshw1  14774  bezout  16487  ptbasfi  23092  filconn  23394  pcopt  24545  ioorinv  25100  itg1addlem2  25221  itg1addlem4  25223  itg1addlem4OLD  25224  itgss  25336  bddmulibl  25363  maxs1  27275  mins2  27278  pthdlem2  29063  mdsymlem6  31699  sumdmdlem2  31710  bj-ax6elem1  35629  wl-equsb4  36508  wl-sbalnae  36513  poimirlem13  36587  poimirlem25  36599  poimirlem27  36601  remullid  41388  sbgoldbaltlem1  46526  setrec2fun  47815