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  842  pm5.71  927  prel12  4150  xpcan2  5376  funun  5561  ablfac1eulem  16687  drngmuleq0  16970  mdetunilem9  18551  maducoeval2  18571  tdeglem4  21655  deg1sublt  21708  dvply1  21876  aaliou2  21932  colline  23187  axcontlem2  23356  3orel3  27505  dfrdg4  28118  arg-ax  28399  elpell14qr2  29344  elpell1qr2  29354  jm2.22  29485  jm2.23  29486  jm2.26lem3  29491  ttac  29526  wepwsolem  29535  dgrnznn  29633  fmul01lt1lem2  29907  3ornot23VD  31886
  Copyright terms: Public domain W3C validator