Theorem orel2 903

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 25	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜓))
2		pm2.21 124	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
3	1, 2	jaod 872	1 ⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓))

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

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 210  df-or 861

This theorem is referenced by:  pm2.64  956  pm2.74  990  pm5.61  1016  pm5.71  1045  3orel3  1517  axprglem  5409  xpcan2  6177  funun  6584  fnpr2ob  17613  ablfac1eulem  20145  drngmuleq0  20848  mdetunilem9  22758  maducoeval2  22778  deg1sublt  26248  dgrnznn  26385  dvply1  26426  aaliou2  26482  oldfib  28548  colline  28901  axcontlem2  29293  dfrdg4  36421  arg-ax  36905  unbdqndv2lem2  37077  elpell14qr2  43569  elpell1qr2  43579  jm2.22  43702  jm2.23  43703  jm2.26lem3  43708  ttac  43743  wepwsolem  43749  3ornot23VD  45535  fmul01lt1lem2  46281  cncfiooicclem1  46587