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

Theorem biorf 405
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 384 . 2  |-  ( ps 
->  ( ph  \/  ps ) )
2 orel1 382 . 2  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
31, 2impbid2 204 1  |-  ( -. 
ph  ->  ( ps  <->  ( ph  \/  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370
This theorem is referenced by:  biortn  406  pm5.61  712  pm5.55  897  3bior1fd  1335  3bior2fd  1337  euor  2317  euor2  2319  eueq3  3260  unineq  3733  ifor  3973  difprsnss  4150  disjprg  4433  disjxun  4435  opthwiener  4739  opthprc  5037  swoord1  7342  brwdomn0  7998  fpwwe2lem13  9023  ne0gt0  9692  xrinfmss  11510  sumsplit  13562  sadadd2lem2  13977  coprm  14118  vdwlem11  14386  lvecvscan  17631  lvecvscan2  17632  mplcoe1  18001  mplcoe5  18005  mplcoe2OLD  18007  maducoeval2  19015  xrsxmet  21187  itg2split  22029  plydiveu  22566  quotcan  22577  coseq1  22787  angrtmuld  23012  leibpilem2  23144  leibpi  23145  wilthlem2  23215  tgldimor  23765  tgcolg  23813  axcontlem7  24145  nb3graprlem2  24324  eupath2lem2  24850  eupath2lem3  24851  nmlnogt0  25584  hvmulcan  25861  hvmulcan2  25862  disjunsn  27325  xrdifh  27463  itgaddnclem2  30049  pr1eqbg  32135  bj-biorfi  33920  elpadd0  35273
  Copyright terms: Public domain W3C validator