Theorem orel1 886

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

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

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 210  df-or 845

This theorem is referenced by:  pm2.25  887  biorf  934  3orel1  1088  xpcan  6000  funun  6370  sorpssuni  7438  sorpssint  7439  soxp  7806  ackbij1lem18  9648  ackbij1b  9650  fincssdom  9734  fin23lem30  9753  fin1a2lem13  9823  pythagtriplem4  16146  zringlpirlem3  20179  psgnodpm  20277  orngsqr  30928  elzdif0  31331  qqhval2lem  31332  eulerpartlemsv2  31726  eulerpartlemv  31732  eulerpartlemf  31738  eulerpartlemgh  31746  3orel13  33060  dfon2lem4  33144  dfon2lem6  33146  nosepdmlem  33300  dfrdg4  33525  rankeq1o  33745  wl-orel12  34916  poimirlem31  35088  pellfund14gap  39828  wepwsolem  39986  fmul01lt1lem1  42226  cncfiooicclem1  42535  etransclem24  42900  nnfoctbdjlem  43094