Theorem orel1 901

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

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

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 210  df-or 861

This theorem is referenced by:  pm2.25  902  biorf  949  3orel1  1107  3orel13  1518  xpcan  6176  funun  6584  sorpssuni  7731  sorpssint  7732  soxp  8126  frxp3  8148  ackbij1lem18  10220  ackbij1b  10222  fincssdom  10308  fin23lem30  10327  fin1a2lem13  10397  pythagtriplem4  16880  orngsqr  20950  zringlpirlem3  21595  psgnodpm  21719  nosepdmlem  27825  0elold  28081  bdayfinbndlem1  28638  elzdif0  34348  qqhval2lem  34349  eulerpartlemsv2  34726  eulerpartlemv  34732  eulerpartlemf  34738  eulerpartlemgh  34746  dfon2lem4  36254  dfon2lem6  36256  dfrdg4  36421  rankeq1o  36641  wl-orel12  38144  poimirlem31  38280  pellfund14gap  43594  wepwsolem  43749  fmul01lt1lem1  46280  cncfiooicclem1  46587  etransclem24  46952  nnfoctbdjlem  47149