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  1489  axprglem  5378  xpcan2  6141  funun  6544  fnpr2ob  17522  ablfac1eulem  20049  drngmuleq0  20740  mdetunilem9  22585  maducoeval2  22605  deg1sublt  26075  dgrnznn  26212  dvply1  26250  aaliou2  26306  oldfib  28369  colline  28717  axcontlem2  29034  dfrdg4  36133  arg-ax  36598  unbdqndv2lem2  36770  elpell14qr2  43290  elpell1qr2  43300  jm2.22  43423  jm2.23  43424  jm2.26lem3  43429  ttac  43464  wepwsolem  43470  3ornot23VD  45273  fmul01lt1lem2  46015  cncfiooicclem1  46321