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

Theorem orel2 373
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 22 . 2  |-  ( -. 
ph  ->  ( ps  ->  ps ) )
2 pm2.21 102 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2jaod 370 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358
This theorem is referenced by:  biorfi  397  pm2.64  765  pm2.74  820  pm5.71  903  prel12  3962  xpcan2  5292  funun  5481  ablfac1eulem  15613  drngmuleq0  15841  tdeglem4  19966  deg1sublt  20016  dvply1  20184  aaliou2  20240  3orel3  25149  dfrdg4  25740  axcontlem2  25847  arg-ax  26109  elpell14qr2  26857  elpell1qr2  26867  jm2.22  26998  jm2.23  26999  jm2.26lem3  27004  ttac  27039  wepwsolem  27048  dgrnznn  27250  fmul01lt1lem2  27624  3ornot23VD  28711
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator