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  6036  funun  6402  fnpr2ob  16833  ablfac1eulem  19196  drngmuleq0  19527  mdetunilem9  21231  maducoeval2  21251  tdeglem4  24656  deg1sublt  24706  dgrnznn  24839  dvply1  24875  aaliou2  24931  colline  26437  axcontlem2  26753  3orel3  32944  dfrdg4  33414  arg-ax  33766  unbdqndv2lem2  33851  elpell14qr2  39466  elpell1qr2  39476  jm2.22  39599  jm2.23  39600  jm2.26lem3  39605  ttac  39640  wepwsolem  39649  3ornot23VD  41188  fmul01lt1lem2  41873  cncfiooicclem1  42183