Theorem pm2.61d2 181

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 179	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  183  jaoi  857  nfald2  2449  2ax6elem  2474  nfsbd  2526  sbal1  2532  nfabd2  2922  rgen2a  3341  posn  5710  frsn  5712  relimasn  6044  nfriotadw  7323  nfriotad  7326  tfinds  7802  curry1val  8047  curry2val  8051  onfununi  8273  findcard2s  9090  prfi  9224  fiint  9227  acndom  9961  dfac12k  10058  iundom2g  10450  nqereu  10840  ltapr  10956  xrmax1  13090  xrmin2  13093  max1ALT  13101  hasheq0  14286  swrdnd2  14579  cshw1  14745  bezout  16470  ptbasfi  23525  filconn  23827  pcopt  24978  ioorinv  25533  itg1addlem2  25654  itg1addlem4  25656  itgss  25769  bddmulibl  25796  maxs1  27737  mins2  27740  pthdlem2  29841  mdsymlem6  32483  sumdmdlem2  32494  bj-ax6elem1  36867  wl-equsb4  37758  wl-sbalnae  37763  poimirlem13  37830  poimirlem25  37842  poimirlem27  37844  remullid  42685  sbgoldbaltlem1  48021  setrec2fun  49933