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  6124  funun  6527  fnpr2ob  17459  ablfac1eulem  19984  drngmuleq0  20676  mdetunilem9  22533  maducoeval2  22553  deg1sublt  26040  dgrnznn  26177  dvply1  26216  aaliou2  26273  colline  28625  axcontlem2  28941  dfrdg4  35984  arg-ax  36449  unbdqndv2lem2  36543  elpell14qr2  42894  elpell1qr2  42904  jm2.22  43027  jm2.23  43028  jm2.26lem3  43033  ttac  43068  wepwsolem  43074  3ornot23VD  44878  fmul01lt1lem2  45624  cncfiooicclem1  45930