Theorem orel1 396

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

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

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 197  df-or 384

This theorem is referenced by:  pm2.25  418  biorf  419  3orel1  1076  prel12OLD  4527  xpcan  5728  funun  6093  sorpssuni  7112  sorpssint  7113  soxp  7459  ackbij1lem18  9271  ackbij1b  9273  fincssdom  9357  fin23lem30  9376  fin1a2lem13  9446  pythagtriplem4  15746  evlslem3  19736  zringlpirlem3  20056  psgnodpm  20156  orngsqr  30134  elzdif0  30354  qqhval2lem  30355  eulerpartlemsv2  30750  eulerpartlemv  30756  eulerpartlemf  30762  eulerpartlemgh  30770  3orel13  31926  dfon2lem4  32017  dfon2lem6  32019  nosepdmlem  32160  dfrdg4  32385  rankeq1o  32605  wl-orel12  33625  poimirlem31  33771  pellfund14gap  37971  wepwsolem  38132  fmul01lt1lem1  40337  cncfiooicclem1  40627  etransclem24  40996  nnfoctbdjlem  41193