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  858  nfald2  2450  2ax6elem  2475  nfsbd  2527  sbal1  2533  nfabd2  2923  rgen2a  3334  posn  5710  frsn  5712  relimasn  6044  nfriotadw  7325  nfriotad  7328  tfinds  7804  curry1val  8048  curry2val  8052  onfununi  8274  findcard2s  9093  prfi  9227  fiint  9230  acndom  9964  dfac12k  10061  iundom2g  10453  nqereu  10843  ltapr  10959  xrmax1  13118  xrmin2  13121  max1ALT  13129  hasheq0  14316  swrdnd2  14609  cshw1  14775  bezout  16503  ptbasfi  23556  filconn  23858  pcopt  24999  ioorinv  25553  itg1addlem2  25674  itg1addlem4  25676  itgss  25789  bddmulibl  25816  maxs1  27747  mins2  27750  pthdlem2  29851  mdsymlem6  32494  sumdmdlem2  32505  bj-ax6elem1  36976  wl-equsb4  37896  wl-sbalnae  37901  poimirlem13  37968  poimirlem25  37980  poimirlem27  37982  remullid  42880  sbgoldbaltlem1  48267  setrec2fun  50179