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  2171  eueq3  2941  unineq  3420  ifor  3606  difprsn  3757  disjprg  4020  disjxun  4022  opthwiener  4267  opthprc  4735  swoord1  6685  brwdomn0  7279  fpwwe2lem13  8260  ne0gt0  8921  xrinfmss  10624  sumsplit  12227  sadadd2lem2  12637  coprm  12775  vdwlem11  13034  lvecvscan  15860  lvecvscan2  15861  mplcoe1  16205  mplcoe2  16207  xrsxmet  18311  itg2split  19100  plydiveu  19674  quotcan  19685  coseq1  19886  angrtmuld  20102  leibpilem2  20233  leibpi  20234  wilthlem2  20303  nmlnogt0  21369  hvmulcan  21647  hvmulcan2  21648  eupath2lem2  23309  eupath2lem3  23310  axcontlem7  24008  elpadd0  29277
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