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

Theorem biorf 394
Description: A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
Assertion
Ref Expression
biorf  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )

Proof of Theorem biorf
StepHypRef Expression
1 olc 373 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 371 . 2  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
31, 2impbid2 195 1  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357
This theorem is referenced by:  biortn  395  pm5.61  693  pm5.55  867  cadan  1382  euor  2172  eueq3  2942  unineq  3421  ifor  3607  difprsn  3758  disjprg  4021  disjxun  4023  opthwiener  4270  opthprc  4738  swoord1  6691  brwdomn0  7285  fpwwe2lem13  8266  ne0gt0  8927  xrinfmss  10630  sumsplit  12233  sadadd2lem2  12643  coprm  12781  vdwlem11  13040  lvecvscan  15866  lvecvscan2  15867  mplcoe1  16211  mplcoe2  16213  xrsxmet  18317  itg2split  19106  plydiveu  19680  quotcan  19691  coseq1  19892  angrtmuld  20108  leibpilem2  20239  leibpi  20240  wilthlem2  20309  nmlnogt0  21377  hvmulcan  21653  hvmulcan2  21654  xrdifh  23275  eupath2lem2  23904  eupath2lem3  23905  axcontlem7  24600  elpadd0  30071
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator