Theorem orel1 885

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

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

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 206  df-or 844

This theorem is referenced by:  pm2.25  886  biorf  933  3orel1  1089  xpcan  6068  funun  6464  sorpssuni  7563  sorpssint  7564  soxp  7941  ackbij1lem18  9924  ackbij1b  9926  fincssdom  10010  fin23lem30  10029  fin1a2lem13  10099  pythagtriplem4  16448  zringlpirlem3  20598  psgnodpm  20705  orngsqr  31405  elzdif0  31830  qqhval2lem  31831  eulerpartlemsv2  32225  eulerpartlemv  32231  eulerpartlemf  32237  eulerpartlemgh  32245  3orel13  33562  dfon2lem4  33668  dfon2lem6  33670  frxp3  33724  nosepdmlem  33813  dfrdg4  34180  rankeq1o  34400  wl-orel12  35597  poimirlem31  35735  pellfund14gap  40625  wepwsolem  40783  fmul01lt1lem1  43015  cncfiooicclem1  43324  etransclem24  43689  nnfoctbdjlem  43883