Theorem pm2.61d2 183

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 181	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  185  jaoi  870  nfald2  2477  2ax6elem  2502  nfsbd  2554  sbal1  2560  nfabd2  2948  rgen2a  3360  posn  5749  frsn  5751  relimasn  6089  nfriotadw  7377  nfriotad  7380  tfinds  7857  curry1val  8101  curry2val  8105  onfununi  8329  findcard2s  9151  prfi  9284  fiint  9287  acndom  10036  dfac12k  10132  iundom2g  10525  nqereu  10915  ltapr  11031  xrmax1  13202  xrmin2  13205  max1ALT  13213  hasheq0  14401  swrdnd2  14695  cshw1  14861  bezout  16602  ptbasfi  23719  filconn  24021  pcopt  25162  ioorinv  25716  itg1addlem2  25837  itg1addlem4  25839  itgss  25952  bddmulibl  25979  maxs1  27914  mins2  27917  pthdlem2  30098  mdsymlem6  32741  sumdmdlem2  32752  vonf1oonfo  35580  bj-ax6elem1  37269  wl-equsb4  38193  wl-sbalnae  38198  poimirlem13  38265  poimirlem25  38277  poimirlem27  38279  remullid  43176  sbgoldbaltlem1  48527  setrec2fun  50453