Theorem orel1 887

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

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

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 206  df-or 847

This theorem is referenced by:  pm2.25  888  biorf  935  3orel1  1089  3orel13  1483  xpcan  6180  funun  6599  sorpssuni  7737  sorpssint  7738  soxp  8134  frxp3  8156  ackbij1lem18  10261  ackbij1b  10263  fincssdom  10347  fin23lem30  10366  fin1a2lem13  10436  pythagtriplem4  16788  zringlpirlem3  21390  psgnodpm  21520  nosepdmlem  27629  0elold  27848  orngsqr  33032  elzdif0  33581  qqhval2lem  33582  eulerpartlemsv2  33978  eulerpartlemv  33984  eulerpartlemf  33990  eulerpartlemgh  33998  dfon2lem4  35382  dfon2lem6  35384  dfrdg4  35547  rankeq1o  35767  wl-orel12  36978  poimirlem31  37124  pellfund14gap  42307  wepwsolem  42466  fmul01lt1lem1  44972  cncfiooicclem1  45281  etransclem24  45646  nnfoctbdjlem  45843