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

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

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 848

This theorem is referenced by:  pm2.25  889  biorf  936  3orel1  1090  3orel13  1489  xpcan  6134  funun  6538  sorpssuni  7677  sorpssint  7678  soxp  8071  frxp3  8093  ackbij1lem18  10146  ackbij1b  10148  fincssdom  10233  fin23lem30  10252  fin1a2lem13  10322  pythagtriplem4  16747  orngsqr  20799  zringlpirlem3  21419  psgnodpm  21543  nosepdmlem  27651  0elold  27906  bdayfinbndlem1  28463  elzdif0  34137  qqhval2lem  34138  eulerpartlemsv2  34515  eulerpartlemv  34521  eulerpartlemf  34527  eulerpartlemgh  34535  dfon2lem4  35978  dfon2lem6  35980  dfrdg4  36145  rankeq1o  36365  wl-orel12  37712  poimirlem31  37848  pellfund14gap  43125  wepwsolem  43280  fmul01lt1lem1  45826  cncfiooicclem1  46133  etransclem24  46498  nnfoctbdjlem  46695