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  5394  xpcan2  6168  funun  6578  fnpr2ob  17710  ablfac1eulem  20268  drngmuleq0  21000  mdetunilem9  22915  maducoeval2  22935  deg1sublt  26408  dgrnznn  26546  dvply1  26587  aaliou2  26649  oldfib  28745  colline  29100  axcontlem2  29525  dfrdg4  36685  arg-ax  37174  unbdqndv2lem2  37346  elpell14qr2  43822  elpell1qr2  43832  jm2.22  43955  jm2.23  43956  jm2.26lem3  43961  ttac  43996  wepwsolem  44002  3ornot23VD  45788  fmul01lt1lem2  46541  cncfiooicclem1  46847