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

Theorem biorf 396
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 375 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 373 . 2  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
31, 2impbid2 197 1  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    \/ wo 359
This theorem is referenced by:  biortn  397  pm5.61  696  pm5.55  872  cadan  1388  euor  2140  eueq3  2877  unineq  3326  ifor  3510  difprsn  3658  disjprg  3916  disjxun  3918  opthwiener  4161  opthprc  4643  swoord1  6575  brwdomn0  7167  fpwwe2lem13  8144  ne0gt0  8805  xrinfmss  10506  sumsplit  12108  sadadd2lem2  12515  coprm  12653  vdwlem11  12912  lvecvscan  15699  lvecvscan2  15700  mplcoe1  16041  mplcoe2  16043  xrsxmet  18147  itg2split  18936  plydiveu  19510  quotcan  19521  coseq1  19722  angrtmuld  19850  leibpilem2  20069  leibpi  20070  wilthlem2  20139  nmlnogt0  21205  hvmulcan  21481  hvmulcan2  21482  eupath2lem2  23073  eupath2lem3  23074  axcontlem7  23772  elpadd0  28687
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator