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  2448  2ax6elem  2473  nfsbd  2525  sbal1  2531  nfabd2  2927  rgen2a  3369  posn  5774  frsn  5776  relimasn  6105  nfriotadw  7396  nfriotad  7399  tfinds  7881  curry1val  8129  curry2val  8133  onfununi  8380  findcard2s  9204  xpfiOLD  9357  prfi  9361  fiint  9364  fiintOLD  9365  acndom  10089  dfac12k  10186  iundom2g  10578  nqereu  10967  ltapr  11083  xrmax1  13214  xrmin2  13217  max1ALT  13225  hasheq0  14399  swrdnd2  14690  cshw1  14857  bezout  16577  ptbasfi  23605  filconn  23907  pcopt  25069  ioorinv  25625  itg1addlem2  25746  itg1addlem4  25748  itg1addlem4OLD  25749  itgss  25862  bddmulibl  25889  maxs1  27825  mins2  27828  pthdlem2  29801  mdsymlem6  32437  sumdmdlem2  32448  bj-ax6elem1  36649  wl-equsb4  37538  wl-sbalnae  37543  poimirlem13  37620  poimirlem25  37632  poimirlem27  37634  remullid  42440  sbgoldbaltlem1  47704  setrec2fun  48923