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

Theorem biorf 395
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 374 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 372 . 2  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
31, 2impbid2 196 1  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358
This theorem is referenced by:  biortn  396  pm5.61  694  pm5.55  868  3bior1fd  1289  3bior2fd  1291  cadan  1398  euor  2267  eueq3  3054  unineq  3536  ifor  3724  difprsnss  3879  disjprg  4151  disjxun  4153  opthwiener  4401  opthprc  4867  swoord1  6872  brwdomn0  7472  fpwwe2lem13  8452  ne0gt0  9113  xrinfmss  10822  sumsplit  12481  sadadd2lem2  12891  coprm  13029  vdwlem11  13288  lvecvscan  16112  lvecvscan2  16113  mplcoe1  16457  mplcoe2  16459  xrsxmet  18713  itg2split  19510  plydiveu  20084  quotcan  20095  coseq1  20299  angrtmuld  20519  leibpilem2  20650  leibpi  20651  wilthlem2  20721  nb3graprlem2  21329  eupath2lem2  21550  eupath2lem3  21551  nmlnogt0  22148  hvmulcan  22424  hvmulcan2  22425  xrdifh  23981  axcontlem7  25625  elpadd0  29925
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 178  df-or 360
  Copyright terms: Public domain W3C validator