Theorem orel1 885

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

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

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 209  df-or 844

This theorem is referenced by:  pm2.25  886  biorf  933  3orel1  1087  xpcan  6035  funun  6402  sorpssuni  7460  sorpssint  7461  soxp  7825  ackbij1lem18  9661  ackbij1b  9663  fincssdom  9747  fin23lem30  9766  fin1a2lem13  9836  pythagtriplem4  16158  zringlpirlem3  20635  psgnodpm  20734  orngsqr  30879  elzdif0  31223  qqhval2lem  31224  eulerpartlemsv2  31618  eulerpartlemv  31624  eulerpartlemf  31630  eulerpartlemgh  31638  3orel13  32949  dfon2lem4  33033  dfon2lem6  33035  nosepdmlem  33189  dfrdg4  33414  rankeq1o  33634  wl-orel12  34753  poimirlem31  34925  pellfund14gap  39491  wepwsolem  39649  fmul01lt1lem1  41872  cncfiooicclem1  42183  etransclem24  42550  nnfoctbdjlem  42744