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  1486  xpcan  6198  funun  6614  sorpssuni  7751  sorpssint  7752  soxp  8153  frxp3  8175  ackbij1lem18  10274  ackbij1b  10276  fincssdom  10361  fin23lem30  10380  fin1a2lem13  10450  pythagtriplem4  16853  zringlpirlem3  21493  psgnodpm  21624  nosepdmlem  27743  0elold  27962  orngsqr  33314  elzdif0  33943  qqhval2lem  33944  eulerpartlemsv2  34340  eulerpartlemv  34346  eulerpartlemf  34352  eulerpartlemgh  34360  dfon2lem4  35768  dfon2lem6  35770  dfrdg4  35933  rankeq1o  36153  wl-orel12  37492  poimirlem31  37638  pellfund14gap  42875  wepwsolem  43031  fmul01lt1lem1  45540  cncfiooicclem1  45849  etransclem24  46214  nnfoctbdjlem  46411