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  5738  frsn  5740  relimasn  6078  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  13192  xrmin2  13195  max1ALT  13203  hasheq0  14390  swrdnd2  14683  cshw1  14849  bezout  16591  ptbasfi  23699  filconn  24001  pcopt  25142  ioorinv  25696  itg1addlem2  25817  itg1addlem4  25819  itgss  25932  bddmulibl  25959  maxs1  27891  mins2  27894  pthdlem2  30026  mdsymlem6  32669  sumdmdlem2  32680  vonf1oonfo  35470  bj-ax6elem1  37150  wl-equsb4  38072  wl-sbalnae  38077  poimirlem13  38144  poimirlem25  38156  poimirlem27  38158  remullid  43055  sbgoldbaltlem1  48399  setrec2fun  50321