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  1043  3orel3  1510  axprglem  5398  xpcan2  6167  funun  6571  fnpr2ob  17602  ablfac1eulem  20135  drngmuleq0  20836  mdetunilem9  22738  maducoeval2  22758  deg1sublt  26228  dgrnznn  26365  dvply1  26406  aaliou2  26462  oldfib  28528  colline  28877  axcontlem2  29224  dfrdg4  36314  arg-ax  36789  unbdqndv2lem2  36961  elpell14qr2  43451  elpell1qr2  43461  jm2.22  43584  jm2.23  43585  jm2.26lem3  43590  ttac  43625  wepwsolem  43631  3ornot23VD  45420  fmul01lt1lem2  46159  cncfiooicclem1  46465