Theorem orel2 398

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

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

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 197  df-or 385

This theorem is referenced by:  biorfi  422  biorfiOLD  423  pm2.64  830  pm2.74  891  pm5.71  977  prel12  4383  xpcan2  5571  funun  5932  ablfac1eulem  18471  drngmuleq0  18770  mdetunilem9  20426  maducoeval2  20446  tdeglem4  23820  deg1sublt  23870  dgrnznn  24003  dvply1  24039  aaliou2  24095  colline  25544  axcontlem2  25845  3orel3  31593  dfrdg4  32058  arg-ax  32415  unbdqndv2lem2  32501  elpell14qr2  37426  elpell1qr2  37436  jm2.22  37562  jm2.23  37563  jm2.26lem3  37568  ttac  37603  wepwsolem  37612  3ornot23VD  39082  fmul01lt1lem2  39817  cncfiooicclem1  40106