Theorem orel1 889

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

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

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 849

This theorem is referenced by:  pm2.25  890  biorf  937  3orel1  1091  3orel13  1490  xpcan  6142  funun  6546  sorpssuni  7687  sorpssint  7688  soxp  8081  frxp3  8103  ackbij1lem18  10158  ackbij1b  10160  fincssdom  10245  fin23lem30  10264  fin1a2lem13  10334  pythagtriplem4  16759  orngsqr  20811  zringlpirlem3  21431  psgnodpm  21555  nosepdmlem  27663  0elold  27918  bdayfinbndlem1  28475  elzdif0  34157  qqhval2lem  34158  eulerpartlemsv2  34535  eulerpartlemv  34541  eulerpartlemf  34547  eulerpartlemgh  34555  dfon2lem4  35997  dfon2lem6  35999  dfrdg4  36164  rankeq1o  36384  wl-orel12  37760  poimirlem31  37896  pellfund14gap  43238  wepwsolem  43393  fmul01lt1lem1  45938  cncfiooicclem1  46245  etransclem24  46610  nnfoctbdjlem  46807