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  6135  funun  6538  fnpr2ob  17479  ablfac1eulem  20003  drngmuleq0  20696  mdetunilem9  22564  maducoeval2  22584  deg1sublt  26071  dgrnznn  26208  dvply1  26247  aaliou2  26304  oldfib  28373  colline  28721  axcontlem2  29038  dfrdg4  36145  arg-ax  36610  unbdqndv2lem2  36710  elpell14qr2  43100  elpell1qr2  43110  jm2.22  43233  jm2.23  43234  jm2.26lem3  43239  ttac  43274  wepwsolem  43280  3ornot23VD  45083  fmul01lt1lem2  45827  cncfiooicclem1  46133