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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.61ii  185  jaoi  871  nfald2  2480  2ax6elem  2505  nfsbd  2557  sbal1  2563  nfabd2  2951  rgen2a  3363  posn  5752  frsn  5754  relimasn  6092  nfriotadw  7388  nfriotad  7391  tfinds  7865  curry1val  8109  curry2val  8113  onfununi  8337  findcard2s  9160  prfi  9293  fiint  9296  acndom  10054  dfac12k  10150  iundom2g  10542  nqereu  10932  ltapr  11048  xrmax1  13219  xrmin2  13222  max1ALT  13230  hasheq0  14419  swrdnd2  14717  cshw1  14885  bezout  16626  ptbasfi  23775  filconn  24077  pcopt  25218  ioorinv  25772  itg1addlem2  25893  itg1addlem4  25895  itgss  26008  bddmulibl  26035  maxs1  27970  mins2  27973  pthdlem2  30154  mdsymlem6  32797  sumdmdlem2  32808  vonf1oonfo  35623  bj-ax6elem1  37329  wl-equsb4  38253  wl-sbalnae  38258  poimirlem13  38325  poimirlem25  38337  poimirlem27  38339  remullid  43236  sbgoldbaltlem1  48585  setrec2fun  50511