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  1488  xpcan  6176  funun  6592  sorpssuni  7734  sorpssint  7735  soxp  8136  frxp3  8158  ackbij1lem18  10258  ackbij1b  10260  fincssdom  10345  fin23lem30  10364  fin1a2lem13  10434  pythagtriplem4  16839  zringlpirlem3  21437  psgnodpm  21560  nosepdmlem  27664  0elold  27883  orngsqr  33274  elzdif0  33940  qqhval2lem  33941  eulerpartlemsv2  34319  eulerpartlemv  34325  eulerpartlemf  34331  eulerpartlemgh  34339  dfon2lem4  35746  dfon2lem6  35748  dfrdg4  35911  rankeq1o  36131  wl-orel12  37471  poimirlem31  37617  pellfund14gap  42861  wepwsolem  43017  fmul01lt1lem1  45556  cncfiooicclem1  45865  etransclem24  46230  nnfoctbdjlem  46427