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  6170  funun  6587  sorpssuni  7731  sorpssint  7732  soxp  8133  frxp3  8155  ackbij1lem18  10255  ackbij1b  10257  fincssdom  10342  fin23lem30  10361  fin1a2lem13  10431  pythagtriplem4  16844  zringlpirlem3  21430  psgnodpm  21553  nosepdmlem  27652  0elold  27878  orngsqr  33331  elzdif0  34016  qqhval2lem  34017  eulerpartlemsv2  34395  eulerpartlemv  34401  eulerpartlemf  34407  eulerpartlemgh  34415  dfon2lem4  35809  dfon2lem6  35811  dfrdg4  35974  rankeq1o  36194  wl-orel12  37534  poimirlem31  37680  pellfund14gap  42877  wepwsolem  43033  fmul01lt1lem1  45580  cncfiooicclem1  45889  etransclem24  46254  nnfoctbdjlem  46451