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

Theorem orel2 383
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 380 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368
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 370
This theorem is referenced by:  biorfi  407  pm2.64  787  pm2.74  843  pm5.71  929  prel12  4196  xpcan2  5435  funun  5621  ablfac1eulem  16906  drngmuleq0  17195  mdetunilem9  18882  maducoeval2  18902  tdeglem4  22186  deg1sublt  22239  dvply1  22407  aaliou2  22463  colline  23736  axcontlem2  23937  3orel3  28414  dfrdg4  29027  arg-ax  29308  elpell14qr2  30253  elpell1qr2  30263  jm2.22  30394  jm2.23  30395  jm2.26lem3  30400  ttac  30435  wepwsolem  30444  dgrnznn  30542  fmul01lt1lem2  30954  cncfiooicclem1  31051  3ornot23VD  32602
  Copyright terms: Public domain W3C validator