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

Theorem orel2 887
 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 123 . 2 𝜑 → (𝜑𝜓))
31, 2jaod 855 1 𝜑 → ((𝜓𝜑) → 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 843 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 209  df-or 844 This theorem is referenced by:  pm2.64  938  pm2.74  971  pm5.61  997  pm5.71  1024  xpcan2  6033  funun  6399  fnpr2ob  16830  ablfac1eulem  19193  drngmuleq0  19524  mdetunilem9  21228  maducoeval2  21248  tdeglem4  24653  deg1sublt  24703  dgrnznn  24836  dvply1  24872  aaliou2  24928  colline  26434  axcontlem2  26750  3orel3  32942  dfrdg4  33412  arg-ax  33764  unbdqndv2lem2  33849  elpell14qr2  39459  elpell1qr2  39469  jm2.22  39592  jm2.23  39593  jm2.26lem3  39598  ttac  39633  wepwsolem  39642  3ornot23VD  41181  fmul01lt1lem2  41866  cncfiooicclem1  42176
 Copyright terms: Public domain W3C validator