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  2143  eueq3  2891  unineq  3361  ifor  3546  difprsn  3697  disjprg  3959  disjxun  3961  opthwiener  4205  opthprc  4689  swoord1  6622  brwdomn0  7216  fpwwe2lem13  8197  ne0gt0  8858  xrinfmss  10559  sumsplit  12161  sadadd2lem2  12568  coprm  12706  vdwlem11  12965  lvecvscan  15791  lvecvscan2  15792  mplcoe1  16136  mplcoe2  16138  xrsxmet  18242  itg2split  19031  plydiveu  19605  quotcan  19616  coseq1  19817  angrtmuld  20033  leibpilem2  20164  leibpi  20165  wilthlem2  20234  nmlnogt0  21300  hvmulcan  21576  hvmulcan2  21577  eupath2lem2  23239  eupath2lem3  23240  axcontlem7  23938  elpadd0  29128
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