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  1485  xpcan2  6199  funun  6614  fnpr2ob  17605  ablfac1eulem  20107  drngmuleq0  20780  mdetunilem9  22642  maducoeval2  22662  deg1sublt  26164  dgrnznn  26301  dvply1  26340  aaliou2  26397  colline  28672  axcontlem2  28995  dfrdg4  35933  arg-ax  36399  unbdqndv2lem2  36493  elpell14qr2  42850  elpell1qr2  42860  jm2.22  42984  jm2.23  42985  jm2.26lem3  42990  ttac  43025  wepwsolem  43031  3ornot23VD  44845  fmul01lt1lem2  45541  cncfiooicclem1  45849