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  857  nfald2  2443  2ax6elem  2468  nfsbd  2520  sbal1  2526  nfabd2  2915  rgen2a  3345  posn  5724  frsn  5726  relimasn  6056  nfriotadw  7352  nfriotad  7355  tfinds  7836  curry1val  8084  curry2val  8088  onfununi  8310  findcard2s  9129  xpfiOLD  9270  prfi  9274  fiint  9277  fiintOLD  9278  acndom  10004  dfac12k  10101  iundom2g  10493  nqereu  10882  ltapr  10998  xrmax1  13135  xrmin2  13138  max1ALT  13146  hasheq0  14328  swrdnd2  14620  cshw1  14787  bezout  16513  ptbasfi  23468  filconn  23770  pcopt  24922  ioorinv  25477  itg1addlem2  25598  itg1addlem4  25600  itgss  25713  bddmulibl  25740  maxs1  27677  mins2  27680  pthdlem2  29698  mdsymlem6  32337  sumdmdlem2  32348  bj-ax6elem1  36654  wl-equsb4  37545  wl-sbalnae  37550  poimirlem13  37627  poimirlem25  37639  poimirlem27  37641  remullid  42422  sbgoldbaltlem1  47777  setrec2fun  49678