Theorem pm2.61d2 183

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 181	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.61ii  185  jaoi  871  nfald2  2474  2ax6elem  2499  nfsbd  2551  sbal1  2557  nfabd2  2945  rgen2a  3356  posn  5736  frsn  5738  relimasn  6082  nfriotadw  7386  nfriotad  7389  tfinds  7872  curry1val  8119  curry2val  8123  onfununi  8353  findcard2s  9185  prfi  9319  fiint  9322  setrec2fun  9977  acndom  10134  dfac12k  10230  iundom2g  10628  nqereu  11018  ltapr  11134  xrmax1  13309  xrmin2  13312  max1ALT  13320  hasheq0  14511  swrdnd2  14810  cshw1  14978  bezout  16722  ptbasfi  23906  filconn  24208  pcopt  25349  ioorinv  25903  itg1addlem2  26024  itg1addlem4  26026  itgss  26138  bddmulibl  26165  fltoprmlem1  27999  maxs1  28132  mins2  28135  pthdlem2  30360  mdsymlem6  33016  sumdmdlem2  33027  ordunmax  35766  vonf1oonfo  35969  bj-ax6elem1  37658  wl-equsb4  38583  wl-sbalnae  38588  poimirlem13  38645  poimirlem25  38657  poimirlem27  38659  remullid  43579  sbgoldbaltlem1  48971