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

This theorem is referenced by:  pm2.25  886  biorf  933  3orel1  1087  xpcan  6033  funun  6400  sorpssuni  7458  sorpssint  7459  soxp  7823  ackbij1lem18  9659  ackbij1b  9661  fincssdom  9745  fin23lem30  9764  fin1a2lem13  9834  pythagtriplem4  16156  zringlpirlem3  20633  psgnodpm  20732  orngsqr  30877  elzdif0  31221  qqhval2lem  31222  eulerpartlemsv2  31616  eulerpartlemv  31622  eulerpartlemf  31628  eulerpartlemgh  31636  3orel13  32947  dfon2lem4  33031  dfon2lem6  33033  nosepdmlem  33187  dfrdg4  33412  rankeq1o  33632  wl-orel12  34766  poimirlem31  34938  pellfund14gap  39504  wepwsolem  39662  fmul01lt1lem1  41885  cncfiooicclem1  42196  etransclem24  42563  nnfoctbdjlem  42757