Theorem orel1 899

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

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

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 859

This theorem is referenced by:  pm2.25  900  biorf  947  3orel1  1101  3orel13  1507  xpcan  6158  funun  6563  sorpssuni  7711  sorpssint  7712  soxp  8104  frxp3  8126  ackbij1lem18  10189  ackbij1b  10191  fincssdom  10277  fin23lem30  10296  fin1a2lem13  10366  pythagtriplem4  16838  orngsqr  20895  zringlpirlem3  21496  psgnodpm  21620  nosepdmlem  27724  0elold  27980  bdayfinbndlem1  28537  elzdif0  34238  qqhval2lem  34239  eulerpartlemsv2  34616  eulerpartlemv  34622  eulerpartlemf  34628  eulerpartlemgh  34636  dfon2lem4  36098  dfon2lem6  36100  dfrdg4  36265  rankeq1o  36485  wl-orel12  37978  poimirlem31  38114  pellfund14gap  43428  wepwsolem  43583  fmul01lt1lem1  46124  cncfiooicclem1  46431  etransclem24  46796  nnfoctbdjlem  46993