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  855  nfald2  2438  2ax6elem  2463  nfsbd  2515  sbal1  2521  nfabd2  2918  rgen2a  3354  posn  5763  frsn  5765  relimasn  6089  nfriotadw  7383  nfriotad  7387  tfinds  7865  curry1val  8110  curry2val  8114  onfununi  8362  findcard2s  9190  xpfiOLD  9344  fiint  9350  acndom  10076  dfac12k  10172  iundom2g  10565  nqereu  10954  ltapr  11070  xrmax1  13189  xrmin2  13192  max1ALT  13200  hasheq0  14358  swrdnd2  14641  cshw1  14808  bezout  16522  ptbasfi  23529  filconn  23831  pcopt  24993  ioorinv  25549  itg1addlem2  25670  itg1addlem4  25672  itg1addlem4OLD  25673  itgss  25785  bddmulibl  25812  maxs1  27744  mins2  27747  pthdlem2  29654  mdsymlem6  32290  sumdmdlem2  32301  bj-ax6elem1  36273  wl-equsb4  37155  wl-sbalnae  37160  poimirlem13  37237  poimirlem25  37249  poimirlem27  37251  remullid  42123  sbgoldbaltlem1  47256  setrec2fun  48309