Theorem orel1 396

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

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

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 197  df-or 384

This theorem is referenced by:  pm2.25  418  biorf  419  3orel1  1058  prel12  4414  xpcan  5605  funun  5970  sorpssuni  6988  sorpssint  6989  soxp  7335  ackbij1lem18  9097  ackbij1b  9099  fincssdom  9183  fin23lem30  9202  fin1a2lem13  9272  pythagtriplem4  15571  evlslem3  19562  zringlpirlem3  19882  psgnodpm  19982  orngsqr  29932  elzdif0  30152  qqhval2lem  30153  eulerpartlemsv2  30548  eulerpartlemv  30554  eulerpartlemf  30560  eulerpartlemgh  30568  3orel13  31724  dfon2lem4  31815  dfon2lem6  31817  nosepdmlem  31958  dfrdg4  32183  rankeq1o  32403  wl-orel12  33424  poimirlem31  33570  pellfund14gap  37768  wepwsolem  37929  fmul01lt1lem1  40134  cncfiooicclem1  40424  etransclem24  40793  nnfoctbdjlem  40990