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  2265  eueq3  3052  unineq  3534  ifor  3722  difprsnss  3877  disjprg  4149  disjxun  4151  opthwiener  4399  opthprc  4865  swoord1  6870  brwdomn0  7470  fpwwe2lem13  8450  ne0gt0  9111  xrinfmss  10820  sumsplit  12479  sadadd2lem2  12889  coprm  13027  vdwlem11  13286  lvecvscan  16110  lvecvscan2  16111  mplcoe1  16455  mplcoe2  16457  xrsxmet  18711  itg2split  19508  plydiveu  20082  quotcan  20093  coseq1  20297  angrtmuld  20517  leibpilem2  20648  leibpi  20649  wilthlem2  20719  nb3graprlem2  21327  eupath2lem2  21548  eupath2lem3  21549  nmlnogt0  22146  hvmulcan  22422  hvmulcan2  22423  xrdifh  23979  axcontlem7  25623  elpadd0  29923
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