Theorem orel1 902

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm2.25  903  biorf  950  3orel1  1107  3orel13  1518  xpcan  6173  funun  6583  sorpssuni  7737  sorpssint  7738  soxp  8131  frxp3  8153  ackbij1lem18  10242  ackbij1b  10244  fincssdom  10329  fin23lem30  10348  fin1a2lem13  10418  pythagtriplem4  16917  orngsqr  21038  zringlpirlem3  21683  psgnodpm  21807  nosepdmlem  27927  0elold  28183  bdayfinbndlem1  28740  elzdif0  34498  qqhval2lem  34499  eulerpartlemsv2  34877  eulerpartlemv  34883  eulerpartlemf  34889  eulerpartlemgh  34897  dfon2lem4  36371  dfon2lem6  36373  dfrdg4  36538  rankeq1o  36759  wl-orel12  38282  poimirlem31  38408  pellfund14gap  43736  wepwsolem  43891  fmul01lt1lem1  46422  cncfiooicclem1  46729  etransclem24  47094  nnfoctbdjlem  47291