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

This theorem is referenced by:  pm2.25  418  biorf  419  prel12  4323  xpcan  5489  funun  5846  sorpssuni  6844  sorpssint  6845  soxp  7177  ackbij1lem18  8942  ackbij1b  8944  fincssdom  9028  fin23lem30  9047  fin1a2lem13  9117  pythagtriplem4  15362  evlslem3  19335  zringlpirlem3  19653  psgnodpm  19753  orngsqr  29135  elzdif0  29352  qqhval2lem  29353  eulerpartlemsv2  29747  eulerpartlemv  29753  eulerpartlemf  29759  eulerpartlemgh  29767  3orel1  30846  3orel13  30853  dfon2lem4  30935  dfon2lem6  30937  dfrdg4  31228  rankeq1o  31448  wl-orel12  32473  poimirlem31  32610  pellfund14gap  36469  wepwsolem  36630  fmul01lt1lem1  38651  cncfiooicclem1  38779  etransclem24  39151  nnfoctbdjlem  39348