Theorem orel2 890

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

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

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 848

This theorem is referenced by:  pm2.64  943  pm2.74  976  pm5.61  1002  pm5.71  1029  3orel3  1488  xpcan2  6130  funun  6532  fnpr2ob  17480  ablfac1eulem  19971  drngmuleq0  20666  mdetunilem9  22523  maducoeval2  22543  deg1sublt  26031  dgrnznn  26168  dvply1  26207  aaliou2  26264  colline  28612  axcontlem2  28928  dfrdg4  35924  arg-ax  36389  unbdqndv2lem2  36483  elpell14qr2  42835  elpell1qr2  42845  jm2.22  42968  jm2.23  42969  jm2.26lem3  42974  ttac  43009  wepwsolem  43015  3ornot23VD  44820  fmul01lt1lem2  45567  cncfiooicclem1  45875