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  6129  funun  6532  sorpssuni  7672  sorpssint  7673  soxp  8069  frxp3  8091  ackbij1lem18  10149  ackbij1b  10151  fincssdom  10236  fin23lem30  10255  fin1a2lem13  10325  pythagtriplem4  16749  orngsqr  20769  zringlpirlem3  21389  psgnodpm  21513  nosepdmlem  27611  0elold  27842  elzdif0  33946  qqhval2lem  33947  eulerpartlemsv2  34325  eulerpartlemv  34331  eulerpartlemf  34337  eulerpartlemgh  34345  dfon2lem4  35759  dfon2lem6  35761  dfrdg4  35924  rankeq1o  36144  wl-orel12  37484  poimirlem31  37630  pellfund14gap  42860  wepwsolem  43015  fmul01lt1lem1  45566  cncfiooicclem1  45875  etransclem24  46240  nnfoctbdjlem  46437