Theorem pm2.61d2 181

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 179	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  183  jaoi  858  nfald2  2450  2ax6elem  2475  nfsbd  2527  sbal1  2533  nfabd2  2923  rgen2a  3343  posn  5718  frsn  5720  relimasn  6052  nfriotadw  7333  nfriotad  7336  tfinds  7812  curry1val  8057  curry2val  8061  onfununi  8283  findcard2s  9102  prfi  9236  fiint  9239  acndom  9973  dfac12k  10070  iundom2g  10462  nqereu  10852  ltapr  10968  xrmax1  13102  xrmin2  13105  max1ALT  13113  hasheq0  14298  swrdnd2  14591  cshw1  14757  bezout  16482  ptbasfi  23537  filconn  23839  pcopt  24990  ioorinv  25545  itg1addlem2  25666  itg1addlem4  25668  itgss  25781  bddmulibl  25808  maxs1  27749  mins2  27752  pthdlem2  29853  mdsymlem6  32495  sumdmdlem2  32506  bj-ax6elem1  36905  wl-equsb4  37806  wl-sbalnae  37811  poimirlem13  37878  poimirlem25  37890  poimirlem27  37892  remullid  42798  sbgoldbaltlem1  48133  setrec2fun  50045