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

Theorem orel2 374
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 23 . 2  |-  ( -. 
ph  ->  ( ps  ->  ps ) )
2 pm2.21 102 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2jaod 371 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    \/ wo 359
This theorem is referenced by:  biorfi  398  pm2.64  767  pm2.74  822  pm5.71  907  prel12  3763  xpcan2  5101  funun  5234  ablfac1eulem  15269  drngmuleq0  15497  tdeglem4  19408  deg1sublt  19458  dvply1  19626  aaliou2  19682  3orel3  23435  dfrdg4  23863  axcontlem2  23968  arg-ax  24230  elpell14qr2  26314  elpell1qr2  26324  jm2.22  26455  jm2.23  26456  jm2.26lem3  26461  ttac  26496  wepwsolem  26505  dgrnznn  26707  fmul01lt1lem2  27083  3ornot23VD  27673
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator