Theorem orel1 888

Description: Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)

Assertion

Ref	Expression
orel1	⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))

Proof of Theorem orel1

Step	Hyp	Ref	Expression
1		pm2.53 850	. 2 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
2	1	com12 32	1 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-or 847

This theorem is referenced by:  pm2.25  889  biorf  936  3orel1  1092  3orel13  1488  xpcan  6176  funun  6595  sorpssuni  7722  sorpssint  7723  soxp  8115  frxp3  8137  ackbij1lem18  10232  ackbij1b  10234  fincssdom  10318  fin23lem30  10337  fin1a2lem13  10407  pythagtriplem4  16752  zringlpirlem3  21034  psgnodpm  21141  nosepdmlem  27186  0elold  27402  orngsqr  32422  elzdif0  32960  qqhval2lem  32961  eulerpartlemsv2  33357  eulerpartlemv  33363  eulerpartlemf  33369  eulerpartlemgh  33377  dfon2lem4  34758  dfon2lem6  34760  dfrdg4  34923  rankeq1o  35143  wl-orel12  36380  poimirlem31  36519  pellfund14gap  41625  wepwsolem  41784  fmul01lt1lem1  44300  cncfiooicclem1  44609  etransclem24  44974  nnfoctbdjlem  45171