Theorem orel1 894

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

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

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 208  df-or 854

This theorem is referenced by:  pm2.25  895  biorf  942  3orel1  1096  3orel13  1495  xpcan  6134  funun  6538  sorpssuni  7682  sorpssint  7683  soxp  8076  frxp3  8098  ackbij1lem18  10156  ackbij1b  10158  fincssdom  10243  fin23lem30  10262  fin1a2lem13  10332  pythagtriplem4  16788  orngsqr  20845  zringlpirlem3  21446  psgnodpm  21570  nosepdmlem  27672  0elold  27927  bdayfinbndlem1  28484  elzdif0  34171  qqhval2lem  34172  eulerpartlemsv2  34549  eulerpartlemv  34555  eulerpartlemf  34561  eulerpartlemgh  34569  dfon2lem4  36019  dfon2lem6  36021  dfrdg4  36186  rankeq1o  36406  wl-orel12  37889  poimirlem31  38025  pellfund14gap  43339  wepwsolem  43494  fmul01lt1lem1  46036  cncfiooicclem1  46343  etransclem24  46708  nnfoctbdjlem  46905