MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biorf Structured version   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  1401  euor  2307  eueq3  3101  unineq  3583  ifor  3771  difprsnss  3926  disjprg  4200  disjxun  4202  opthwiener  4450  opthprc  4917  swoord1  6926  brwdomn0  7529  fpwwe2lem13  8509  ne0gt0  9170  xrinfmss  10880  sumsplit  12544  sadadd2lem2  12954  coprm  13092  vdwlem11  13351  lvecvscan  16175  lvecvscan2  16176  mplcoe1  16520  mplcoe2  16522  xrsxmet  18832  itg2split  19633  plydiveu  20207  quotcan  20218  coseq1  20422  angrtmuld  20642  leibpilem2  20773  leibpi  20774  wilthlem2  20844  nb3graprlem2  21453  eupath2lem2  21692  eupath2lem3  21693  nmlnogt0  22290  hvmulcan  22566  hvmulcan2  22567  xrdifh  24135  axcontlem7  25901  itgaddnclem2  26254  pr1eqbg  28046  elpadd0  30543
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