Theorem pm2.61d2 173

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 171	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  177  jaoi  883  nfald2  2425  nfsbd  2536  2ax6elem  2541  sbal1  2552  sbal2  2553  nfabd2  2927  rgen2a  3124  posn  5357  frsn  5359  relimasn  5670  nfriotad  6811  tfinds  7257  curry1val  7472  curry2val  7476  onfununi  7642  findcard2s  8408  xpfi  8438  fiint  8444  acndom  9125  dfac12k  9222  iundom2g  9615  nqereu  10004  ltapr  10120  xrmax1  12208  xrmin2  12211  max1ALT  12219  hasheq0  13356  swrdnd2  13635  cshw1  13851  bezout  15541  ptbasfi  21664  filconn  21966  pcopt  23100  ioorinv  23634  itg1addlem2  23755  itg1addlem4  23757  itgss  23869  bddmulibl  23896  pthdlem2  26956  mdsymlem6  29723  sumdmdlem2  29734  bj-ax6elem1  33087  wl-equsb4  33764  wl-sbalnae  33770  poimirlem13  33846  poimirlem25  33858  poimirlem27  33860  sbgoldbaltlem1  42343  setrec2fun  43108