Theorem orel2 904

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

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

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 862

This theorem is used by:  pm2.64  956  pm2.74  990  pm5.61  1016  pm5.71  1045  3orel3  1517  axprglem  5405  xpcan2  6174  funun  6583  fnpr2ob  17650  ablfac1eulem  20207  drngmuleq0  20935  mdetunilem9  22848  maducoeval2  22868  deg1sublt  26342  dgrnznn  26480  dvply1  26521  aaliou2  26583  oldfib  28650  colline  29005  axcontlem2  29430  dfrdg4  36538  arg-ax  37043  unbdqndv2lem2  37215  elpell14qr2  43711  elpell1qr2  43721  jm2.22  43844  jm2.23  43845  jm2.26lem3  43850  ttac  43885  wepwsolem  43891  3ornot23VD  45677  fmul01lt1lem2  46423  cncfiooicclem1  46729