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  6129  funun  6532  fnpr2ob  17464  ablfac1eulem  19988  drngmuleq0  20680  mdetunilem9  22536  maducoeval2  22556  deg1sublt  26043  dgrnznn  26180  dvply1  26219  aaliou2  26276  colline  28628  axcontlem2  28945  dfrdg4  36016  arg-ax  36481  unbdqndv2lem2  36575  elpell14qr2  42979  elpell1qr2  42989  jm2.22  43112  jm2.23  43113  jm2.26lem3  43118  ttac  43153  wepwsolem  43159  3ornot23VD  44963  fmul01lt1lem2  45709  cncfiooicclem1  46015