Theorem orel2 891

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

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

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 849

This theorem is referenced by:  pm2.64  944  pm2.74  977  pm5.61  1003  pm5.71  1030  3orel3  1489  axprglem  5373  xpcan2  6135  funun  6538  fnpr2ob  17513  ablfac1eulem  20040  drngmuleq0  20731  mdetunilem9  22595  maducoeval2  22615  deg1sublt  26085  dgrnznn  26222  dvply1  26260  aaliou2  26317  oldfib  28383  colline  28731  axcontlem2  29048  dfrdg4  36149  arg-ax  36614  unbdqndv2lem2  36786  elpell14qr2  43308  elpell1qr2  43318  jm2.22  43441  jm2.23  43442  jm2.26lem3  43447  ttac  43482  wepwsolem  43488  3ornot23VD  45291  fmul01lt1lem2  46033  cncfiooicclem1  46339