Theorem orel2 890

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

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

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 847

This theorem is referenced by:  pm2.64  941  pm2.74  974  pm5.61  1000  pm5.71  1027  3orel3  1487  xpcan2  6177  funun  6595  fnpr2ob  17504  ablfac1eulem  19942  drngmuleq0  20388  mdetunilem9  22122  maducoeval2  22142  tdeglem4OLD  25578  deg1sublt  25628  dgrnznn  25761  dvply1  25797  aaliou2  25853  colline  27900  axcontlem2  28223  dfrdg4  34923  arg-ax  35301  unbdqndv2lem2  35386  elpell14qr2  41600  elpell1qr2  41610  jm2.22  41734  jm2.23  41735  jm2.26lem3  41740  ttac  41775  wepwsolem  41784  3ornot23VD  43608  fmul01lt1lem2  44301  cncfiooicclem1  44609