Theorem orel2 890

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

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

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 848

This theorem is referenced by:  pm2.64  943  pm2.74  976  pm5.61  1002  pm5.71  1029  3orel3  1488  xpcan2  6166  funun  6582  fnpr2ob  17572  ablfac1eulem  20055  drngmuleq0  20723  mdetunilem9  22558  maducoeval2  22578  deg1sublt  26067  dgrnznn  26204  dvply1  26243  aaliou2  26300  colline  28628  axcontlem2  28944  dfrdg4  35969  arg-ax  36434  unbdqndv2lem2  36528  elpell14qr2  42885  elpell1qr2  42895  jm2.22  43019  jm2.23  43020  jm2.26lem3  43025  ttac  43060  wepwsolem  43066  3ornot23VD  44871  fmul01lt1lem2  45614  cncfiooicclem1  45922