Theorem orel2 904

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 25	. 2 ⊢ (¬ 𝜑 → (𝜓 → 𝜓))
2		pm2.21 124	. 2 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
3	1, 2	jaod 873	1 ⊢ (¬ 𝜑 → ((𝜓 ∨ 𝜑) → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  pm2.64  956  pm2.74  990  pm5.61  1016  pm5.71  1045  3orel3  1517  axprglem  5398  xpcan2  6181  funun  6606  fnpr2ob  17759  ablfac1eulem  20318  drngmuleq0  21050  mdetunilem9  22965  maducoeval2  22985  deg1sublt  26458  dgrnznn  26596  dvply1  26635  aaliou2  26697  oldfib  28793  colline  29148  axcontlem2  29573  cgrainag  33090  maxssj0  36006  onf1oracwevd  36052  dfrdg4  36893  arg-ax  37382  unbdqndv2lem2  37554  elpell14qr2  44062  elpell1qr2  44072  jm2.22  44195  jm2.23  44196  jm2.26lem3  44201  ttac  44236  wepwsolem  44242  3ornot23VD  46020  fmul01lt1lem2  46802  cncfiooicclem1  47108