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  856  nfald2  2445  2ax6elem  2470  nfsbd  2522  sbal1  2528  nfabd2  2930  rgen2a  3368  posn  5762  frsn  5764  relimasn  6084  nfriotadw  7373  nfriotad  7377  tfinds  7849  curry1val  8091  curry2val  8095  onfununi  8341  findcard2s  9165  xpfiOLD  9318  fiint  9324  acndom  10046  dfac12k  10142  iundom2g  10535  nqereu  10924  ltapr  11040  xrmax1  13154  xrmin2  13157  max1ALT  13165  hasheq0  14323  swrdnd2  14605  cshw1  14772  bezout  16485  ptbasfi  23085  filconn  23387  pcopt  24538  ioorinv  25093  itg1addlem2  25214  itg1addlem4  25216  itg1addlem4OLD  25217  itgss  25329  bddmulibl  25356  maxs1  27268  mins2  27271  pthdlem2  29025  mdsymlem6  31661  sumdmdlem2  31672  bj-ax6elem1  35543  wl-equsb4  36422  wl-sbalnae  36427  poimirlem13  36501  poimirlem25  36513  poimirlem27  36515  remullid  41306  sbgoldbaltlem1  46447  setrec2fun  47737