MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orel2 Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 idd 24 . 2 𝜑 → (𝜓𝜓))
2 pm2.21 120 . 2 𝜑 → (𝜑𝜓))
31, 2jaod 394 1 𝜑 → ((𝜓𝜑) → 𝜓))
Colors of variables: wff setvar class
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 197  df-or 384
This theorem is referenced by:  biorfi  421  biorfiOLD  422  pm2.64  847  pm2.74  909  pm5.71  997  prel12  4414  xpcan2  5606  funun  5970  ablfac1eulem  18517  drngmuleq0  18818  mdetunilem9  20474  maducoeval2  20494  tdeglem4  23865  deg1sublt  23915  dgrnznn  24048  dvply1  24084  aaliou2  24140  colline  25589  axcontlem2  25890  3orel3  31719  dfrdg4  32183  arg-ax  32540  unbdqndv2lem2  32626  elpell14qr2  37743  elpell1qr2  37753  jm2.22  37879  jm2.23  37880  jm2.26lem3  37885  ttac  37920  wepwsolem  37929  3ornot23VD  39396  fmul01lt1lem2  40135  cncfiooicclem1  40424
  Copyright terms: Public domain W3C validator