Theorem orel2 887

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

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

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 206  df-or 844

This theorem is referenced by:  pm2.64  938  pm2.74  971  pm5.61  997  pm5.71  1024  xpcan2  6069  funun  6464  fnpr2ob  17186  ablfac1eulem  19590  drngmuleq0  19929  mdetunilem9  21677  maducoeval2  21697  tdeglem4OLD  25130  deg1sublt  25180  dgrnznn  25313  dvply1  25349  aaliou2  25405  colline  26914  axcontlem2  27236  3orel3  33557  dfrdg4  34180  arg-ax  34532  unbdqndv2lem2  34617  elpell14qr2  40600  elpell1qr2  40610  jm2.22  40733  jm2.23  40734  jm2.26lem3  40739  ttac  40774  wepwsolem  40783  3ornot23VD  42356  fmul01lt1lem2  43016  cncfiooicclem1  43324