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 851	. 2 ⊢ ((𝜑 ∨ 𝜓) → (¬ 𝜑 → 𝜓))
2	1	com12 32	1 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))

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

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 207  df-or 848

This theorem is referenced by:  pm2.25  889  biorf  936  3orel1  1090  3orel13  1489  xpcan  6123  funun  6527  sorpssuni  7665  sorpssint  7666  soxp  8059  frxp3  8081  ackbij1lem18  10124  ackbij1b  10126  fincssdom  10211  fin23lem30  10230  fin1a2lem13  10300  pythagtriplem4  16728  orngsqr  20779  zringlpirlem3  21399  psgnodpm  21523  nosepdmlem  27620  0elold  27853  elzdif0  33988  qqhval2lem  33989  eulerpartlemsv2  34366  eulerpartlemv  34372  eulerpartlemf  34378  eulerpartlemgh  34386  dfon2lem4  35819  dfon2lem6  35821  dfrdg4  35984  rankeq1o  36204  wl-orel12  37544  poimirlem31  37690  pellfund14gap  42919  wepwsolem  43074  fmul01lt1lem1  45623  cncfiooicclem1  45930  etransclem24  46295  nnfoctbdjlem  46492