Theorem orel1 887

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

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

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 847

This theorem is referenced by:  pm2.25  888  biorf  935  3orel1  1091  3orel13  1486  xpcan  6207  funun  6624  sorpssuni  7767  sorpssint  7768  soxp  8170  frxp3  8192  ackbij1lem18  10305  ackbij1b  10307  fincssdom  10392  fin23lem30  10411  fin1a2lem13  10481  pythagtriplem4  16866  zringlpirlem3  21498  psgnodpm  21629  nosepdmlem  27746  0elold  27965  orngsqr  33299  elzdif0  33926  qqhval2lem  33927  eulerpartlemsv2  34323  eulerpartlemv  34329  eulerpartlemf  34335  eulerpartlemgh  34343  dfon2lem4  35750  dfon2lem6  35752  dfrdg4  35915  rankeq1o  36135  wl-orel12  37465  poimirlem31  37611  pellfund14gap  42843  wepwsolem  42999  fmul01lt1lem1  45505  cncfiooicclem1  45814  etransclem24  46179  nnfoctbdjlem  46376