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 857	1 ⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓))

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

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 206  df-or 846

This theorem is referenced by:  pm2.64  940  pm2.74  973  pm5.61  999  pm5.71  1026  3orel3  1486  xpcan2  6162  funun  6580  fnpr2ob  17483  ablfac1eulem  19898  drngmuleq0  20290  mdetunilem9  22046  maducoeval2  22066  tdeglem4OLD  25502  deg1sublt  25552  dgrnznn  25685  dvply1  25721  aaliou2  25777  colline  27760  axcontlem2  28083  dfrdg4  34737  arg-ax  35089  unbdqndv2lem2  35174  elpell14qr2  41357  elpell1qr2  41367  jm2.22  41491  jm2.23  41492  jm2.26lem3  41497  ttac  41532  wepwsolem  41541  3ornot23VD  43365  fmul01lt1lem2  44060  cncfiooicclem1  44368