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 119 . 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 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
 Copyright terms: Public domain W3C validator