Theorem orel1 889

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

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

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 849

This theorem is referenced by:  pm2.25  890  biorf  937  3orel1  1091  3orel13  1490  xpcan  6134  funun  6538  sorpssuni  7679  sorpssint  7680  soxp  8072  frxp3  8094  ackbij1lem18  10149  ackbij1b  10151  fincssdom  10236  fin23lem30  10255  fin1a2lem13  10325  pythagtriplem4  16781  orngsqr  20834  zringlpirlem3  21454  psgnodpm  21578  nosepdmlem  27661  0elold  27916  bdayfinbndlem1  28473  elzdif0  34140  qqhval2lem  34141  eulerpartlemsv2  34518  eulerpartlemv  34524  eulerpartlemf  34530  eulerpartlemgh  34538  dfon2lem4  35982  dfon2lem6  35984  dfrdg4  36149  rankeq1o  36369  wl-orel12  37850  poimirlem31  37986  pellfund14gap  43333  wepwsolem  43488  fmul01lt1lem1  46032  cncfiooicclem1  46339  etransclem24  46704  nnfoctbdjlem  46901