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

Theorem biorf 396
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 375 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 373 . 2  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
31, 2impbid2 197 1  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    \/ wo 359
This theorem is referenced by:  biortn  397  pm5.61  696  pm5.55  872  cadan  1388  euor  2145  eueq3  2915  unineq  3394  ifor  3579  difprsn  3730  disjprg  3993  disjxun  3995  opthwiener  4240  opthprc  4724  swoord1  6657  brwdomn0  7251  fpwwe2lem13  8232  ne0gt0  8893  xrinfmss  10595  sumsplit  12197  sadadd2lem2  12604  coprm  12742  vdwlem11  13001  lvecvscan  15827  lvecvscan2  15828  mplcoe1  16172  mplcoe2  16174  xrsxmet  18278  itg2split  19067  plydiveu  19641  quotcan  19652  coseq1  19853  angrtmuld  20069  leibpilem2  20200  leibpi  20201  wilthlem2  20270  nmlnogt0  21336  hvmulcan  21612  hvmulcan2  21613  eupath2lem2  23275  eupath2lem3  23276  axcontlem7  23974  elpadd0  29248
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator