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  2476  2ax6elem  2501  nfsbd  2553  sbal1  2559  nfabd2  2947  rgen2a  3358  posn  5745  frsn  5747  relimasn  6085  nfriotadw  7382  nfriotad  7385  tfinds  7860  curry1val  8106  curry2val  8110  onfununi  8334  findcard2s  9164  prfi  9297  fiint  9300  acndom  10058  dfac12k  10154  iundom2g  10552  nqereu  10942  ltapr  11058  xrmax1  13231  xrmin2  13234  max1ALT  13242  hasheq0  14431  swrdnd2  14729  cshw1  14897  bezout  16639  ptbasfi  23813  filconn  24115  pcopt  25256  ioorinv  25810  itg1addlem2  25931  itg1addlem4  25933  itgss  26046  bddmulibl  26073  maxs1  28013  mins2  28016  pthdlem2  30241  mdsymlem6  32897  sumdmdlem2  32908  vonf1oonfo  35720  bj-ax6elem1  37404  wl-equsb4  38328  wl-sbalnae  38333  poimirlem13  38390  poimirlem25  38402  poimirlem27  38404  remullid  43317  sbgoldbaltlem1  48703  setrec2fun  50626