Theorem orel2 896

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

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

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 208  df-or 854

This theorem is referenced by:  pm2.64  949  pm2.74  982  pm5.61  1008  pm5.71  1035  3orel3  1494  axprglem  5372  xpcan2  6135  funun  6538  fnpr2ob  17520  ablfac1eulem  20047  drngmuleq0  20742  mdetunilem9  22610  maducoeval2  22630  deg1sublt  26100  dgrnznn  26237  dvply1  26275  aaliou2  26331  oldfib  28394  colline  28742  axcontlem2  29059  dfrdg4  36186  arg-ax  36651  unbdqndv2lem2  36823  elpell14qr2  43314  elpell1qr2  43324  jm2.22  43447  jm2.23  43448  jm2.26lem3  43453  ttac  43488  wepwsolem  43494  3ornot23VD  45297  fmul01lt1lem2  46037  cncfiooicclem1  46343