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  5412  xpcan2  6180  funun  6589  fnpr2ob  17637  ablfac1eulem  20175  drngmuleq0  20903  mdetunilem9  22814  maducoeval2  22834  deg1sublt  26304  dgrnznn  26441  dvply1  26482  aaliou2  26540  oldfib  28607  colline  28960  axcontlem2  29352  dfrdg4  36464  arg-ax  36968  unbdqndv2lem2  37140  elpell14qr2  43630  elpell1qr2  43640  jm2.22  43763  jm2.23  43764  jm2.26lem3  43769  ttac  43804  wepwsolem  43810  3ornot23VD  45596  fmul01lt1lem2  46342  cncfiooicclem1  46648