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  6152  funun  6565  sorpssuni  7711  sorpssint  7712  soxp  8111  frxp3  8133  ackbij1lem18  10196  ackbij1b  10198  fincssdom  10283  fin23lem30  10302  fin1a2lem13  10372  pythagtriplem4  16797  zringlpirlem3  21381  psgnodpm  21504  nosepdmlem  27602  0elold  27828  orngsqr  33289  elzdif0  33977  qqhval2lem  33978  eulerpartlemsv2  34356  eulerpartlemv  34362  eulerpartlemf  34368  eulerpartlemgh  34376  dfon2lem4  35781  dfon2lem6  35783  dfrdg4  35946  rankeq1o  36166  wl-orel12  37506  poimirlem31  37652  pellfund14gap  42882  wepwsolem  43038  fmul01lt1lem1  45589  cncfiooicclem1  45898  etransclem24  46263  nnfoctbdjlem  46460