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

Theorem orel2 383
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  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )

Proof of Theorem orel2
StepHypRef Expression
1 idd 24 . 2  |-  ( -. 
ph  ->  ( ps  ->  ps ) )
2 pm2.21 108 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2jaod 380 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368
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 185  df-or 370
This theorem is referenced by:  biorfi  407  pm2.64  787  pm2.74  842  pm5.71  927  prel12  4044  xpcan2  5270  funun  5455  ablfac1eulem  16561  drngmuleq0  16833  mdetunilem9  18401  maducoeval2  18421  tdeglem4  21504  deg1sublt  21557  dvply1  21725  aaliou2  21781  colline  23020  axcontlem2  23162  3orel3  27319  dfrdg4  27932  arg-ax  28214  elpell14qr2  29156  elpell1qr2  29166  jm2.22  29297  jm2.23  29298  jm2.26lem3  29303  ttac  29338  wepwsolem  29347  dgrnznn  29445  fmul01lt1lem2  29719  3ornot23VD  31470
  Copyright terms: Public domain W3C validator