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  2285  eueq3  3073  unineq  3555  ifor  3743  difprsnss  3898  disjprg  4172  disjxun  4174  opthwiener  4422  opthprc  4888  swoord1  6897  brwdomn0  7497  fpwwe2lem13  8477  ne0gt0  9138  xrinfmss  10848  sumsplit  12511  sadadd2lem2  12921  coprm  13059  vdwlem11  13318  lvecvscan  16142  lvecvscan2  16143  mplcoe1  16487  mplcoe2  16489  xrsxmet  18797  itg2split  19598  plydiveu  20172  quotcan  20183  coseq1  20387  angrtmuld  20607  leibpilem2  20738  leibpi  20739  wilthlem2  20809  nb3graprlem2  21418  eupath2lem2  21657  eupath2lem3  21658  nmlnogt0  22255  hvmulcan  22531  hvmulcan2  22532  xrdifh  24100  axcontlem7  25817  itgaddnclem2  26167  pr1eqbg  27948  elpadd0  30295
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