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

Theorem orel2 381
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 24 . 2  |-  ( -. 
ph  ->  ( ps  ->  ps ) )
2 pm2.21 108 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2jaod 378 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 366
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 185  df-or 368
This theorem is referenced by:  biorfi  405  pm2.64  787  pm2.74  844  pm5.71  934  prel12  4193  xpcan2  5429  funun  5612  ablfac1eulem  17318  drngmuleq0  17614  mdetunilem9  19289  maducoeval2  19309  tdeglem4  22624  deg1sublt  22677  dgrnznn  22810  dvply1  22846  aaliou2  22902  colline  24231  axcontlem2  24470  3orel3  29330  dfrdg4  29828  arg-ax  30109  elpell14qr2  31037  elpell1qr2  31047  jm2.22  31176  jm2.23  31177  jm2.26lem3  31182  ttac  31217  wepwsolem  31226  fmul01lt1lem2  31818  cncfiooicclem1  31935  3ornot23VD  34047
  Copyright terms: Public domain W3C validator