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  6149  funun  6562  sorpssuni  7708  sorpssint  7709  soxp  8108  frxp3  8130  ackbij1lem18  10189  ackbij1b  10191  fincssdom  10276  fin23lem30  10295  fin1a2lem13  10365  pythagtriplem4  16790  zringlpirlem3  21374  psgnodpm  21497  nosepdmlem  27595  0elold  27821  orngsqr  33282  elzdif0  33970  qqhval2lem  33971  eulerpartlemsv2  34349  eulerpartlemv  34355  eulerpartlemf  34361  eulerpartlemgh  34369  dfon2lem4  35774  dfon2lem6  35776  dfrdg4  35939  rankeq1o  36159  wl-orel12  37499  poimirlem31  37645  pellfund14gap  42875  wepwsolem  43031  fmul01lt1lem1  45582  cncfiooicclem1  45891  etransclem24  46256  nnfoctbdjlem  46453