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

This theorem is referenced by:  pm2.64  939  pm2.74  972  pm5.61  998  pm5.71  1025  3orel3  1485  xpcan2  6080  funun  6480  fnpr2ob  17269  ablfac1eulem  19675  drngmuleq0  20014  mdetunilem9  21769  maducoeval2  21789  tdeglem4OLD  25225  deg1sublt  25275  dgrnznn  25408  dvply1  25444  aaliou2  25500  colline  27010  axcontlem2  27333  dfrdg4  34253  arg-ax  34605  unbdqndv2lem2  34690  elpell14qr2  40684  elpell1qr2  40694  jm2.22  40817  jm2.23  40818  jm2.26lem3  40823  ttac  40858  wepwsolem  40867  3ornot23VD  42467  fmul01lt1lem2  43126  cncfiooicclem1  43434