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  2183  eueq3  2953  unineq  3432  ifor  3618  difprsnss  3769  disjprg  4035  disjxun  4037  opthwiener  4284  opthprc  4752  swoord1  6705  brwdomn0  7299  fpwwe2lem13  8280  ne0gt0  8941  xrinfmss  10644  sumsplit  12247  sadadd2lem2  12657  coprm  12795  vdwlem11  13054  lvecvscan  15880  lvecvscan2  15881  mplcoe1  16225  mplcoe2  16227  xrsxmet  18331  itg2split  19120  plydiveu  19694  quotcan  19705  coseq1  19906  angrtmuld  20122  leibpilem2  20253  leibpi  20254  wilthlem2  20323  nmlnogt0  21391  hvmulcan  21667  hvmulcan2  21668  xrdifh  23288  eupath2lem2  23917  eupath2lem3  23918  axcontlem7  24670  3bior1fd  28177  3bior2fd  28179  nb3graprlem2  28288  elpadd0  30620
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