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  3790  xpcan2  5112  funun  5261  ablfac1eulem  15301  drngmuleq0  15529  tdeglem4  19440  deg1sublt  19490  dvply1  19658  aaliou2  19714  3orel3  23467  dfrdg4  23895  axcontlem2  24000  arg-ax  24262  elpell14qr2  26346  elpell1qr2  26356  jm2.22  26487  jm2.23  26488  jm2.26lem3  26493  ttac  26528  wepwsolem  26537  dgrnznn  26739  fmul01lt1lem2  27114  3ornot23VD  27891
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