Theorem orel2 901

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

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

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 209  df-or 859

This theorem is referenced by:  pm2.64  954  pm2.74  987  pm5.61  1013  pm5.71  1040  3orel3  1506  axprglem  5392  xpcan2  6159  funun  6563  fnpr2ob  17571  ablfac1eulem  20097  drngmuleq0  20792  mdetunilem9  22660  maducoeval2  22680  deg1sublt  26150  dgrnznn  26287  dvply1  26325  aaliou2  26381  oldfib  28447  colline  28795  axcontlem2  29112  dfrdg4  36265  arg-ax  36740  unbdqndv2lem2  36912  elpell14qr2  43403  elpell1qr2  43413  jm2.22  43536  jm2.23  43537  jm2.26lem3  43542  ttac  43577  wepwsolem  43583  3ornot23VD  45386  fmul01lt1lem2  46125  cncfiooicclem1  46431