Theorem orel2 887

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

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

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 209  df-or 844

This theorem is referenced by:  pm2.64  938  pm2.74  971  pm5.61  997  pm5.71  1024  xpcan2  6033  funun  6399  fnpr2ob  16830  ablfac1eulem  19193  drngmuleq0  19524  mdetunilem9  21228  maducoeval2  21248  tdeglem4  24653  deg1sublt  24703  dgrnznn  24836  dvply1  24872  aaliou2  24928  colline  26434  axcontlem2  26750  3orel3  32942  dfrdg4  33412  arg-ax  33764  unbdqndv2lem2  33849  elpell14qr2  39457  elpell1qr2  39467  jm2.22  39590  jm2.23  39591  jm2.26lem3  39596  ttac  39631  wepwsolem  39640  3ornot23VD  41179  fmul01lt1lem2  41864  cncfiooicclem1  42174