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

Theorem orel2 915
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 121 . 2 𝜑 → (𝜑𝜓))
31, 2jaod 886 1 𝜑 → ((𝜓𝜑) → 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 874
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 199  df-or 875
This theorem is referenced by:  biorfi  963  pm2.64  966  pm2.74  998  pm5.71  1053  prel12OLD  4569  xpcan2  5789  funun  6147  ablfac1eulem  18786  drngmuleq0  19087  mdetunilem9  20751  maducoeval2  20771  tdeglem4  24160  deg1sublt  24210  dgrnznn  24343  dvply1  24379  aaliou2  24435  colline  25899  axcontlem2  26201  3orel3  32107  dfrdg4  32570  arg-ax  32922  unbdqndv2lem2  33008  elpell14qr2  38207  elpell1qr2  38217  jm2.22  38342  jm2.23  38343  jm2.26lem3  38348  ttac  38383  wepwsolem  38392  3ornot23VD  39838  fmul01lt1lem2  40556  cncfiooicclem1  40845
  Copyright terms: Public domain W3C validator