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  868  nfald2  2475  2ax6elem  2500  nfsbd  2552  sbal1  2558  nfabd2  2946  rgen2a  3357  posn  5731  frsn  5733  relimasn  6071  nfriotadw  7357  nfriotad  7360  tfinds  7836  curry1val  8079  curry2val  8083  onfununi  8307  findcard2s  9130  prfi  9264  fiint  9267  acndom  10004  dfac12k  10101  iundom2g  10494  nqereu  10884  ltapr  11000  xrmax1  13175  xrmin2  13178  max1ALT  13186  hasheq0  14373  swrdnd2  14666  cshw1  14832  bezout  16560  ptbasfi  23621  filconn  23923  pcopt  25064  ioorinv  25618  itg1addlem2  25739  itg1addlem4  25741  itgss  25854  bddmulibl  25881  maxs1  27810  mins2  27813  pthdlem2  29914  mdsymlem6  32557  sumdmdlem2  32568  vonf1oonfo  35422  bj-ax6elem1  37102  wl-equsb4  38024  wl-sbalnae  38029  poimirlem13  38096  poimirlem25  38108  poimirlem27  38110  remullid  43007  sbgoldbaltlem1  48365  setrec2fun  50277