Theorem orel2 889

Description: Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 5-Apr-2013.)

Assertion

Ref	Expression
orel2	⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓))

Proof of Theorem orel2

Step	Hyp	Ref	Expression
1		idd 24	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜓))
2		pm2.21 123	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
3	1, 2	jaod 858	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.64  942  pm2.74  975  pm5.61  1001  pm5.71  1028  3orel3  1485  xpcan2  6208  funun  6624  fnpr2ob  17618  ablfac1eulem  20116  drngmuleq0  20785  mdetunilem9  22647  maducoeval2  22667  deg1sublt  26169  dgrnznn  26306  dvply1  26343  aaliou2  26400  colline  28675  axcontlem2  28998  dfrdg4  35915  arg-ax  36382  unbdqndv2lem2  36476  elpell14qr2  42818  elpell1qr2  42828  jm2.22  42952  jm2.23  42953  jm2.26lem3  42958  ttac  42993  wepwsolem  42999  3ornot23VD  44818  fmul01lt1lem2  45506  cncfiooicclem1  45814