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

Theorem orel2 372
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 21 . 2  |-  ( -. 
ph  ->  ( ps  ->  ps ) )
2 pm2.21 100 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2jaod 369 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357
This theorem is referenced by:  biorfi  396  pm2.64  764  pm2.74  819  pm5.71  902  prel12  3805  xpcan2  5129  funun  5312  ablfac1eulem  15323  drngmuleq0  15551  tdeglem4  19462  deg1sublt  19512  dvply1  19680  aaliou2  19736  3orel3  24078  dfrdg4  24560  axcontlem2  24665  arg-ax  24927  elpell14qr2  27050  elpell1qr2  27060  jm2.22  27191  jm2.23  27192  jm2.26lem3  27197  ttac  27232  wepwsolem  27241  dgrnznn  27443  fmul01lt1lem2  27818  3ornot23VD  28939
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 177  df-or 359
  Copyright terms: Public domain W3C validator