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  2475  2ax6elem  2500  nfsbd  2552  sbal1  2558  nfabd2  2946  rgen2a  3357  posn  5737  frsn  5739  relimasn  6079  nfriotadw  7377  nfriotad  7380  tfinds  7860  curry1val  8105  curry2val  8109  onfununi  8333  findcard2s  9165  prfi  9299  fiint  9302  setrec2fun  9954  acndom  10111  dfac12k  10207  iundom2g  10605  nqereu  10995  ltapr  11111  xrmax1  13286  xrmin2  13289  max1ALT  13297  hasheq0  14487  swrdnd2  14785  cshw1  14953  bezout  16696  ptbasfi  23880  filconn  24182  pcopt  25323  ioorinv  25877  itg1addlem2  25998  itg1addlem4  26000  itgss  26112  bddmulibl  26139  fltoprmlem1  27975  maxs1  28108  mins2  28111  pthdlem2  30336  mdsymlem6  32992  sumdmdlem2  33003  vonf1oonfo  35867  bj-ax6elem1  37535  wl-equsb4  38457  wl-sbalnae  38462  poimirlem13  38519  poimirlem25  38531  poimirlem27  38533  remullid  43453  sbgoldbaltlem1  48821