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  2447  2ax6elem  2472  nfsbd  2524  sbal1  2530  nfabd2  2919  rgen2a  3338  posn  5705  frsn  5707  relimasn  6038  nfriotadw  7317  nfriotad  7320  tfinds  7796  curry1val  8041  curry2val  8045  onfununi  8267  findcard2s  9082  prfi  9215  fiint  9218  acndom  9949  dfac12k  10046  iundom2g  10438  nqereu  10827  ltapr  10943  xrmax1  13076  xrmin2  13079  max1ALT  13087  hasheq0  14272  swrdnd2  14565  cshw1  14731  bezout  16456  ptbasfi  23497  filconn  23799  pcopt  24950  ioorinv  25505  itg1addlem2  25626  itg1addlem4  25628  itgss  25741  bddmulibl  25768  maxs1  27705  mins2  27708  pthdlem2  29748  mdsymlem6  32390  sumdmdlem2  32401  bj-ax6elem1  36731  wl-equsb4  37622  wl-sbalnae  37627  poimirlem13  37693  poimirlem25  37705  poimirlem27  37707  remullid  42552  sbgoldbaltlem1  47903  setrec2fun  49817