Theorem orel2 888

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

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

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 210  df-or 845

This theorem is referenced by:  pm2.64  939  pm2.74  972  pm5.61  998  pm5.71  1025  xpcan2  6001  funun  6370  fnpr2ob  16823  ablfac1eulem  19187  drngmuleq0  19518  mdetunilem9  21225  maducoeval2  21245  tdeglem4  24661  deg1sublt  24711  dgrnznn  24844  dvply1  24880  aaliou2  24936  colline  26443  axcontlem2  26759  3orel3  33055  dfrdg4  33525  arg-ax  33877  unbdqndv2lem2  33962  elpell14qr2  39803  elpell1qr2  39813  jm2.22  39936  jm2.23  39937  jm2.26lem3  39942  ttac  39977  wepwsolem  39986  3ornot23VD  41553  fmul01lt1lem2  42227  cncfiooicclem1  42535