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  5382  xpcan2  6143  funun  6546  fnpr2ob  17491  ablfac1eulem  20015  drngmuleq0  20708  mdetunilem9  22576  maducoeval2  22596  deg1sublt  26083  dgrnznn  26220  dvply1  26259  aaliou2  26316  oldfib  28385  colline  28733  axcontlem2  29050  dfrdg4  36164  arg-ax  36629  unbdqndv2lem2  36729  elpell14qr2  43213  elpell1qr2  43223  jm2.22  43346  jm2.23  43347  jm2.26lem3  43352  ttac  43387  wepwsolem  43393  3ornot23VD  45196  fmul01lt1lem2  45939  cncfiooicclem1  46245