Theorem orel1 886

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

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

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 206  df-or 845

This theorem is referenced by:  pm2.25  887  biorf  934  3orel1  1090  xpcan  6079  funun  6480  sorpssuni  7585  sorpssint  7586  soxp  7970  ackbij1lem18  9993  ackbij1b  9995  fincssdom  10079  fin23lem30  10098  fin1a2lem13  10168  pythagtriplem4  16520  zringlpirlem3  20686  psgnodpm  20793  orngsqr  31503  elzdif0  31930  qqhval2lem  31931  eulerpartlemsv2  32325  eulerpartlemv  32331  eulerpartlemf  32337  eulerpartlemgh  32345  3orel13  33660  dfon2lem4  33762  dfon2lem6  33764  frxp3  33797  nosepdmlem  33886  dfrdg4  34253  rankeq1o  34473  wl-orel12  35670  poimirlem31  35808  pellfund14gap  40709  wepwsolem  40867  fmul01lt1lem1  43125  cncfiooicclem1  43434  etransclem24  43799  nnfoctbdjlem  43993