Theorem orel2 915

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 121	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
3	1, 2	jaod 886	1 ⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓))

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

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 199  df-or 875

This theorem is referenced by:  biorfi  963  pm2.64  966  pm2.74  998  pm5.71  1053  prel12OLD  4569  xpcan2  5789  funun  6147  ablfac1eulem  18786  drngmuleq0  19087  mdetunilem9  20751  maducoeval2  20771  tdeglem4  24160  deg1sublt  24210  dgrnznn  24343  dvply1  24379  aaliou2  24435  colline  25899  axcontlem2  26201  3orel3  32107  dfrdg4  32570  arg-ax  32922  unbdqndv2lem2  33008  elpell14qr2  38207  elpell1qr2  38217  jm2.22  38342  jm2.23  38343  jm2.26lem3  38348  ttac  38383  wepwsolem  38392  3ornot23VD  39838  fmul01lt1lem2  40556  cncfiooicclem1  40845