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

Theorem orel2 384
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 25 . 2  |-  ( -. 
ph  ->  ( ps  ->  ps ) )
2 pm2.21 111 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2jaod 381 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-or 371
This theorem is referenced by:  biorfi  408  pm2.64  796  pm2.74  854  pm5.71  944  prel12  4171  xpcan2  5285  funun  5634  ablfac1eulem  17633  drngmuleq0  17926  mdetunilem9  19569  maducoeval2  19589  tdeglem4  22883  deg1sublt  22933  dgrnznn  23066  dvply1  23102  aaliou2  23158  colline  24551  axcontlem2  24838  3orel3  30129  dfrdg4  30500  arg-ax  30858  elpell14qr2  35418  elpell1qr2  35428  jm2.22  35560  jm2.23  35561  jm2.26lem3  35566  ttac  35601  wepwsolem  35610  3ornot23VD  36887  fmul01lt1lem2  37239  cncfiooicclem1  37347
  Copyright terms: Public domain W3C validator