Theorem orel2 397

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

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

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 196  df-or 384

This theorem is referenced by:  biorfi  421  biorfiOLD  422  pm2.64  826  pm2.74  887  pm5.71  973  prel12  4323  xpcan2  5490  funun  5846  ablfac1eulem  18294  drngmuleq0  18593  mdetunilem9  20245  maducoeval2  20265  tdeglem4  23624  deg1sublt  23674  dgrnznn  23807  dvply1  23843  aaliou2  23899  colline  25344  axcontlem2  25645  3orel3  30848  dfrdg4  31228  arg-ax  31585  unbdqndv2lem2  31671  elpell14qr2  36444  elpell1qr2  36454  jm2.22  36580  jm2.23  36581  jm2.26lem3  36586  ttac  36621  wepwsolem  36630  3ornot23VD  38104  fmul01lt1lem2  38652  cncfiooicclem1  38779