Theorem pm2.61d2 174

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 172	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  178  jaoi  888  nfald2  2466  nfsbd  2577  2ax6elem  2583  sbal1  2593  sbal2OLD  2595  nfabd2  2989  rgen2a  3186  posn  5422  frsn  5424  relimasn  5729  nfriotad  6874  tfinds  7320  curry1val  7534  curry2val  7538  onfununi  7704  findcard2s  8470  xpfi  8500  fiint  8506  acndom  9187  dfac12k  9284  iundom2g  9677  nqereu  10066  ltapr  10182  xrmax1  12294  xrmin2  12297  max1ALT  12305  hasheq0  13444  swrdnd2  13720  cshw1  13943  bezout  15633  ptbasfi  21755  filconn  22057  pcopt  23191  ioorinv  23742  itg1addlem2  23863  itg1addlem4  23865  itgss  23977  bddmulibl  24004  pthdlem2  27070  mdsymlem6  29811  sumdmdlem2  29822  bj-ax6elem1  33180  wl-equsb4  33876  wl-sbalnae  33882  poimirlem13  33959  poimirlem25  33971  poimirlem27  33973  sbgoldbaltlem1  42490  setrec2fun  43327