Theorem pm2.61d2 184

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 182	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  186  jaoi  854  nfald2  2456  2ax6elem  2482  nfsbd  2541  sbal1  2548  nfabd2  2978  rgen2a  3193  posn  5601  frsn  5603  relimasn  5919  nfriotadw  7101  nfriotad  7104  tfinds  7554  curry1val  7783  curry2val  7787  onfununi  7961  findcard2s  8743  xpfi  8773  fiint  8779  acndom  9462  dfac12k  9558  iundom2g  9951  nqereu  10340  ltapr  10456  xrmax1  12556  xrmin2  12559  max1ALT  12567  hasheq0  13720  swrdnd2  14008  cshw1  14175  bezout  15881  ptbasfi  22186  filconn  22488  pcopt  23627  ioorinv  24180  itg1addlem2  24301  itg1addlem4  24303  itgss  24415  bddmulibl  24442  pthdlem2  27557  mdsymlem6  30191  sumdmdlem2  30202  bj-ax6elem1  34112  wl-equsb4  34958  wl-sbalnae  34963  poimirlem13  35070  poimirlem25  35082  poimirlem27  35084  remulid2  39570  sbgoldbaltlem1  44297  setrec2fun  45222