Theorem orel2 890

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 847

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 848

This theorem is referenced by:  pm2.64  943  pm2.74  976  pm5.61  1002  pm5.71  1029  3orel3  1488  xpcan2  6150  funun  6562  fnpr2ob  17521  ablfac1eulem  20004  drngmuleq0  20672  mdetunilem9  22507  maducoeval2  22527  deg1sublt  26015  dgrnznn  26152  dvply1  26191  aaliou2  26248  colline  28576  axcontlem2  28892  dfrdg4  35939  arg-ax  36404  unbdqndv2lem2  36498  elpell14qr2  42850  elpell1qr2  42860  jm2.22  42984  jm2.23  42985  jm2.26lem3  42990  ttac  43025  wepwsolem  43031  3ornot23VD  44836  fmul01lt1lem2  45583  cncfiooicclem1  45891