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  2445  2ax6elem  2470  nfsbd  2522  sbal1  2528  nfabd2  2918  rgen2a  3337  posn  5702  frsn  5704  relimasn  6034  nfriotadw  7311  nfriotad  7314  tfinds  7790  curry1val  8035  curry2val  8039  onfununi  8261  findcard2s  9075  prfi  9208  fiint  9211  acndom  9939  dfac12k  10036  iundom2g  10428  nqereu  10817  ltapr  10933  xrmax1  13071  xrmin2  13074  max1ALT  13082  hasheq0  14267  swrdnd2  14560  cshw1  14726  bezout  16451  ptbasfi  23494  filconn  23796  pcopt  24947  ioorinv  25502  itg1addlem2  25623  itg1addlem4  25625  itgss  25738  bddmulibl  25765  maxs1  27702  mins2  27705  pthdlem2  29744  mdsymlem6  32383  sumdmdlem2  32394  bj-ax6elem1  36699  wl-equsb4  37590  wl-sbalnae  37595  poimirlem13  37672  poimirlem25  37684  poimirlem27  37686  remullid  42466  sbgoldbaltlem1  47809  setrec2fun  49723