Theorem orel2 903

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 25	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜓))
2		pm2.21 124	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
3	1, 2	jaod 872	1 ⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 861

This theorem is used by:  pm2.64  955  pm2.74  989  pm5.61  1015  pm5.71  1044  3orel3  1516  axprglem  5406  xpcan2  6174  funun  6582  fnpr2ob  17618  ablfac1eulem  20150  drngmuleq0  20877  mdetunilem9  22788  maducoeval2  22808  deg1sublt  26278  dgrnznn  26415  dvply1  26456  aaliou2  26514  oldfib  28581  colline  28934  axcontlem2  29326  dfrdg4  36451  arg-ax  36955  unbdqndv2lem2  37127  elpell14qr2  43617  elpell1qr2  43627  jm2.22  43750  jm2.23  43751  jm2.26lem3  43756  ttac  43791  wepwsolem  43797  3ornot23VD  45583  fmul01lt1lem2  46329  cncfiooicclem1  46635