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  2479  2ax6elem  2504  nfsbd  2556  sbal1  2562  nfabd2  2950  rgen2a  3361  posn  5737  frsn  5739  relimasn  6077  nfriotadw  7365  nfriotad  7368  tfinds  7844  curry1val  8088  curry2val  8092  onfununi  8316  findcard2s  9138  prfi  9271  fiint  9274  acndom  10023  dfac12k  10119  iundom2g  10512  nqereu  10902  ltapr  11018  xrmax1  13189  xrmin2  13192  max1ALT  13200  hasheq0  14387  swrdnd2  14681  cshw1  14847  bezout  16589  ptbasfi  23695  filconn  23997  pcopt  25138  ioorinv  25692  itg1addlem2  25813  itg1addlem4  25815  itgss  25928  bddmulibl  25955  maxs1  27887  mins2  27890  pthdlem2  30022  mdsymlem6  32665  sumdmdlem2  32676  vonf1oonfo  35465  bj-ax6elem1  37145  wl-equsb4  38067  wl-sbalnae  38072  poimirlem13  38139  poimirlem25  38151  poimirlem27  38153  remullid  43050  sbgoldbaltlem1  48400  setrec2fun  50322