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

Theorem orel2 396
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 118 . 2 𝜑 → (𝜑𝜓))
31, 2jaod 393 1 𝜑 → ((𝜓𝜑) → 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 381
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 195  df-or 383
This theorem is referenced by:  biorfi  420  biorfiOLD  421  pm2.64  825  pm2.74  886  pm5.71  972  prel12  4318  xpcan2  5476  funun  5832  ablfac1eulem  18243  drngmuleq0  18542  mdetunilem9  20193  maducoeval2  20213  tdeglem4  23569  deg1sublt  23619  dgrnznn  23752  dvply1  23788  aaliou2  23844  colline  25290  axcontlem2  25591  3orel3  30682  dfrdg4  31062  arg-ax  31419  unbdqndv2lem2  31505  elpell14qr2  36268  elpell1qr2  36278  jm2.22  36404  jm2.23  36405  jm2.26lem3  36410  ttac  36445  wepwsolem  36454  3ornot23VD  37928  fmul01lt1lem2  38476  cncfiooicclem1  38603
  Copyright terms: Public domain W3C validator