Theorem pm2.61d2 182

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 180	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  184  jaoi  866  nfald2  2466  2ax6elem  2491  nfsbd  2543  sbal1  2549  nfabd2  2937  rgen2a  3348  posn  5722  frsn  5724  relimasn  6060  nfriotadw  7346  nfriotad  7349  tfinds  7825  curry1val  8068  curry2val  8072  onfununi  8296  findcard2s  9119  prfi  9253  fiint  9256  acndom  9993  dfac12k  10090  iundom2g  10483  nqereu  10873  ltapr  10989  xrmax1  13164  xrmin2  13167  max1ALT  13175  hasheq0  14362  swrdnd2  14655  cshw1  14821  bezout  16549  ptbasfi  23610  filconn  23912  pcopt  25053  ioorinv  25607  itg1addlem2  25728  itg1addlem4  25730  itgss  25843  bddmulibl  25870  maxs1  27799  mins2  27802  pthdlem2  29903  mdsymlem6  32546  sumdmdlem2  32557  bj-ax6elem1  37076  wl-equsb4  37998  wl-sbalnae  38003  poimirlem13  38070  poimirlem25  38082  poimirlem27  38084  remullid  42981  sbgoldbaltlem1  48339  setrec2fun  50251