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  3336  posn  5709  frsn  5711  relimasn  6040  nfriotadw  7318  nfriotad  7321  tfinds  7800  curry1val  8045  curry2val  8049  onfununi  8271  findcard2s  9089  xpfiOLD  9228  prfi  9232  fiint  9235  fiintOLD  9236  acndom  9964  dfac12k  10061  iundom2g  10453  nqereu  10842  ltapr  10958  xrmax1  13095  xrmin2  13098  max1ALT  13106  hasheq0  14288  swrdnd2  14580  cshw1  14746  bezout  16472  ptbasfi  23484  filconn  23786  pcopt  24938  ioorinv  25493  itg1addlem2  25614  itg1addlem4  25616  itgss  25729  bddmulibl  25756  maxs1  27693  mins2  27696  pthdlem2  29731  mdsymlem6  32370  sumdmdlem2  32381  bj-ax6elem1  36639  wl-equsb4  37530  wl-sbalnae  37535  poimirlem13  37612  poimirlem25  37624  poimirlem27  37626  remullid  42407  sbgoldbaltlem1  47764  setrec2fun  49678