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  3689  xpcan2  5020  funun  5153  ablfac1eulem  15142  drngmuleq0  15370  tdeglem4  19278  deg1sublt  19328  dvply1  19496  aaliou2  19552  3orel3  23234  dfrdg4  23662  axcontlem2  23767  arg-ax  24029  elpell14qr2  26113  elpell1qr2  26123  jm2.22  26254  jm2.23  26255  jm2.26lem3  26260  ttac  26295  wepwsolem  26304  dgrnznn  26506  fmul01lt1lem2  26882  3ornot23VD  27410
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