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  1488  xpcan2  6197  funun  6612  fnpr2ob  17603  ablfac1eulem  20092  drngmuleq0  20763  mdetunilem9  22626  maducoeval2  22646  deg1sublt  26149  dgrnznn  26286  dvply1  26325  aaliou2  26382  colline  28657  axcontlem2  28980  dfrdg4  35952  arg-ax  36417  unbdqndv2lem2  36511  elpell14qr2  42873  elpell1qr2  42883  jm2.22  43007  jm2.23  43008  jm2.26lem3  43013  ttac  43048  wepwsolem  43054  3ornot23VD  44867  fmul01lt1lem2  45600  cncfiooicclem1  45908