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  854  nfald2  2445  2ax6elem  2470  nfsbd  2526  sbal1  2533  nfabd2  2933  rgen2a  3158  posn  5672  frsn  5674  relimasn  5992  nfriotadw  7240  nfriotad  7244  tfinds  7706  curry1val  7945  curry2val  7949  onfununi  8172  findcard2s  8948  xpfi  9085  fiint  9091  acndom  9807  dfac12k  9903  iundom2g  10296  nqereu  10685  ltapr  10801  xrmax1  12909  xrmin2  12912  max1ALT  12920  hasheq0  14078  swrdnd2  14368  cshw1  14535  bezout  16251  ptbasfi  22732  filconn  23034  pcopt  24185  ioorinv  24740  itg1addlem2  24861  itg1addlem4  24863  itg1addlem4OLD  24864  itgss  24976  bddmulibl  25003  pthdlem2  28136  mdsymlem6  30770  sumdmdlem2  30781  bj-ax6elem1  34847  wl-equsb4  35712  wl-sbalnae  35717  poimirlem13  35790  poimirlem25  35802  poimirlem27  35804  remulid2  40415  sbgoldbaltlem1  45231  setrec2fun  46398