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

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

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 846

This theorem is referenced by:  pm2.64  939  pm2.74  972  pm5.61  998  pm5.71  1025  3orel3  1481  xpcan2  6186  funun  6604  fnpr2ob  17547  ablfac1eulem  20036  drngmuleq0  20662  mdetunilem9  22542  maducoeval2  22562  tdeglem4OLD  26016  deg1sublt  26066  dgrnznn  26201  dvply1  26238  aaliou2  26295  colline  28473  axcontlem2  28796  dfrdg4  35580  arg-ax  35933  unbdqndv2lem2  36018  elpell14qr2  42313  elpell1qr2  42323  jm2.22  42447  jm2.23  42448  jm2.26lem3  42453  ttac  42488  wepwsolem  42497  3ornot23VD  44317  fmul01lt1lem2  45002  cncfiooicclem1  45310

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »