Theorem orel1 901

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

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

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 861

This theorem is referenced by:  pm2.25  902  biorf  949  3orel1  1105  3orel13  1511  xpcan  6166  funun  6571  sorpssuni  7719  sorpssint  7720  soxp  8113  frxp3  8135  ackbij1lem18  10207  ackbij1b  10209  fincssdom  10295  fin23lem30  10314  fin1a2lem13  10384  pythagtriplem4  16869  orngsqr  20938  zringlpirlem3  21574  psgnodpm  21698  nosepdmlem  27805  0elold  28061  bdayfinbndlem1  28618  elzdif0  34287  qqhval2lem  34288  eulerpartlemsv2  34665  eulerpartlemv  34671  eulerpartlemf  34677  eulerpartlemgh  34685  dfon2lem4  36147  dfon2lem6  36149  dfrdg4  36314  rankeq1o  36534  wl-orel12  38026  poimirlem31  38162  pellfund14gap  43476  wepwsolem  43631  fmul01lt1lem1  46158  cncfiooicclem1  46465  etransclem24  46830  nnfoctbdjlem  47027