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  1516  axprglem  5393  xpcan2  6168  funun  6586  fnpr2ob  17735  ablfac1eulem  20293  drngmuleq0  21025  mdetunilem9  22940  maducoeval2  22960  deg1sublt  26433  dgrnznn  26571  dvply1  26610  aaliou2  26672  oldfib  28768  colline  29123  axcontlem2  29548  cgrainag  33065  maxssj0  35945  onf1oracwevd  35971  dfrdg4  36807  arg-ax  37296  unbdqndv2lem2  37468  elpell14qr2  43962  elpell1qr2  43972  jm2.22  44095  jm2.23  44096  jm2.26lem3  44101  ttac  44136  wepwsolem  44142  3ornot23VD  45922  fmul01lt1lem2  46690  cncfiooicclem1  46996