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  6128  funun  6532  sorpssuni  7671  sorpssint  7672  soxp  8065  frxp3  8087  ackbij1lem18  10134  ackbij1b  10136  fincssdom  10221  fin23lem30  10240  fin1a2lem13  10310  pythagtriplem4  16733  orngsqr  20783  zringlpirlem3  21403  psgnodpm  21527  nosepdmlem  27623  0elold  27856  elzdif0  34014  qqhval2lem  34015  eulerpartlemsv2  34392  eulerpartlemv  34398  eulerpartlemf  34404  eulerpartlemgh  34412  dfon2lem4  35849  dfon2lem6  35851  dfrdg4  36016  rankeq1o  36236  wl-orel12  37576  poimirlem31  37711  pellfund14gap  43004  wepwsolem  43159  fmul01lt1lem1  45708  cncfiooicclem1  46015  etransclem24  46380  nnfoctbdjlem  46577