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  6153  funun  6565  fnpr2ob  17528  ablfac1eulem  20011  drngmuleq0  20679  mdetunilem9  22514  maducoeval2  22534  deg1sublt  26022  dgrnznn  26159  dvply1  26198  aaliou2  26255  colline  28583  axcontlem2  28899  dfrdg4  35946  arg-ax  36411  unbdqndv2lem2  36505  elpell14qr2  42857  elpell1qr2  42867  jm2.22  42991  jm2.23  42992  jm2.26lem3  42997  ttac  43032  wepwsolem  43038  3ornot23VD  44843  fmul01lt1lem2  45590  cncfiooicclem1  45898