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  2170  eueq3  2940  unineq  3419  ifor  3605  difprsn  3756  disjprg  4019  disjxun  4021  opthwiener  4268  opthprc  4736  swoord1  6689  brwdomn0  7283  fpwwe2lem13  8264  ne0gt0  8925  xrinfmss  10628  sumsplit  12231  sadadd2lem2  12641  coprm  12779  vdwlem11  13038  lvecvscan  15864  lvecvscan2  15865  mplcoe1  16209  mplcoe2  16211  xrsxmet  18315  itg2split  19104  plydiveu  19678  quotcan  19689  coseq1  19890  angrtmuld  20106  leibpilem2  20237  leibpi  20238  wilthlem2  20307  nmlnogt0  21375  hvmulcan  21651  hvmulcan2  21652  xrdifh  23273  eupath2lem2  23902  eupath2lem3  23903  axcontlem7  24598  elpadd0  29998
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