Theorem orel1 889

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

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

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 849

This theorem is referenced by:  pm2.25  890  biorf  937  3orel1  1091  3orel13  1490  xpcan  6140  funun  6544  sorpssuni  7686  sorpssint  7687  soxp  8079  frxp3  8101  ackbij1lem18  10158  ackbij1b  10160  fincssdom  10245  fin23lem30  10264  fin1a2lem13  10334  pythagtriplem4  16790  orngsqr  20843  zringlpirlem3  21444  psgnodpm  21568  nosepdmlem  27647  0elold  27902  bdayfinbndlem1  28459  elzdif0  34124  qqhval2lem  34125  eulerpartlemsv2  34502  eulerpartlemv  34508  eulerpartlemf  34514  eulerpartlemgh  34522  dfon2lem4  35966  dfon2lem6  35968  dfrdg4  36133  rankeq1o  36353  wl-orel12  37836  poimirlem31  37972  pellfund14gap  43315  wepwsolem  43470  fmul01lt1lem1  46014  cncfiooicclem1  46321  etransclem24  46686  nnfoctbdjlem  46883