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  853  nfald2  2445  2ax6elem  2470  nfsbd  2526  sbal1  2533  nfabd2  2932  rgen2a  3155  posn  5663  frsn  5665  relimasn  5981  nfriotadw  7220  nfriotad  7224  tfinds  7681  curry1val  7916  curry2val  7920  onfununi  8143  findcard2s  8910  xpfi  9015  fiint  9021  acndom  9738  dfac12k  9834  iundom2g  10227  nqereu  10616  ltapr  10732  xrmax1  12838  xrmin2  12841  max1ALT  12849  hasheq0  14006  swrdnd2  14296  cshw1  14463  bezout  16179  ptbasfi  22640  filconn  22942  pcopt  24091  ioorinv  24645  itg1addlem2  24766  itg1addlem4  24768  itg1addlem4OLD  24769  itgss  24881  bddmulibl  24908  pthdlem2  28037  mdsymlem6  30671  sumdmdlem2  30682  bj-ax6elem1  34774  wl-equsb4  35639  wl-sbalnae  35644  poimirlem13  35717  poimirlem25  35729  poimirlem27  35731  remulid2  40336  sbgoldbaltlem1  45119  setrec2fun  46284