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

Theorem orel2 385
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 112 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2jaod 382 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 370
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 189  df-or 372
This theorem is referenced by:  biorfi  409  pm2.64  798  pm2.74  857  pm5.71  947  prel12  4152  xpcan2  5274  funun  5624  ablfac1eulem  17705  drngmuleq0  17998  mdetunilem9  19645  maducoeval2  19665  tdeglem4  23009  deg1sublt  23059  dgrnznn  23201  dvply1  23237  aaliou2  23296  colline  24694  axcontlem2  24995  3orel3  30344  dfrdg4  30718  arg-ax  31076  elpell14qr2  35708  elpell1qr2  35718  jm2.22  35850  jm2.23  35851  jm2.26lem3  35856  ttac  35891  wepwsolem  35900  3ornot23VD  37243  fmul01lt1lem2  37663  cncfiooicclem1  37771
  Copyright terms: Public domain W3C validator