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  2450  2ax6elem  2475  nfsbd  2527  sbal1  2533  nfabd2  2923  rgen2a  3355  posn  5745  frsn  5747  relimasn  6077  nfriotadw  7375  nfriotad  7378  tfinds  7860  curry1val  8109  curry2val  8113  onfununi  8360  findcard2s  9184  xpfiOLD  9336  prfi  9340  fiint  9343  fiintOLD  9344  acndom  10070  dfac12k  10167  iundom2g  10559  nqereu  10948  ltapr  11064  xrmax1  13196  xrmin2  13199  max1ALT  13207  hasheq0  14386  swrdnd2  14678  cshw1  14845  bezout  16567  ptbasfi  23524  filconn  23826  pcopt  24978  ioorinv  25534  itg1addlem2  25655  itg1addlem4  25657  itgss  25770  bddmulibl  25797  maxs1  27734  mins2  27737  pthdlem2  29755  mdsymlem6  32394  sumdmdlem2  32405  bj-ax6elem1  36689  wl-equsb4  37580  wl-sbalnae  37585  poimirlem13  37662  poimirlem25  37674  poimirlem27  37676  remullid  42443  sbgoldbaltlem1  47760  setrec2fun  49523