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  2477  2ax6elem  2502  nfsbd  2554  sbal1  2560  nfabd2  2949  rgen2a  3360  posn  5743  frsn  5745  relimasn  6096  nfriotadw  7411  nfriotad  7414  tfinds  7898  curry1val  8146  curry2val  8150  onfununi  8380  findcard2s  9212  prfi  9346  fiint  9349  setrec2fun  10003  acndom  10160  dfac12k  10256  iundom2g  10654  nqereu  11044  ltapr  11160  xrmax1  13335  xrmin2  13338  max1ALT  13346  hasheq0  14537  swrdnd2  14836  cshw1  15004  bezout  16748  ptbasfi  23933  filconn  24235  pcopt  25376  ioorinv  25930  itg1addlem2  26051  itg1addlem4  26053  itgss  26165  bddmulibl  26192  fltoprmlem1  28026  maxs1  28159  mins2  28162  pthdlem2  30387  mdsymlem6  33043  sumdmdlem2  33054  ordunmax  35805  vonf1oonfo  36062  bj-ax6elem1  37756  wl-equsb4  38694  wl-sbalnae  38699  poimirlem13  38756  poimirlem25  38768  poimirlem27  38770  remullid  43689  sbgoldbaltlem1  49092