Theorem orel1 888

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

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

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 210  df-or 847

This theorem is referenced by:  pm2.25  889  biorf  936  3orel1  1092  xpcan  6008  funun  6385  sorpssuni  7476  sorpssint  7477  soxp  7849  ackbij1lem18  9737  ackbij1b  9739  fincssdom  9823  fin23lem30  9842  fin1a2lem13  9912  pythagtriplem4  16256  zringlpirlem3  20305  psgnodpm  20404  orngsqr  31080  elzdif0  31500  qqhval2lem  31501  eulerpartlemsv2  31895  eulerpartlemv  31901  eulerpartlemf  31907  eulerpartlemgh  31915  3orel13  33233  dfon2lem4  33334  dfon2lem6  33336  frxp3  33408  nosepdmlem  33527  dfrdg4  33891  rankeq1o  34111  wl-orel12  35293  poimirlem31  35431  pellfund14gap  40281  wepwsolem  40439  fmul01lt1lem1  42667  cncfiooicclem1  42976  etransclem24  43341  nnfoctbdjlem  43535