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

Theorem biorf 398
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

Proof of Theorem biorf
StepHypRef Expression
1 olc 377 . 2
2 orel1 375 . 2
31, 2impbid2 198 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 178  \/wo 361
This theorem is referenced by:  biortn  399  pm5.61  697  pm5.55  877  3bior1fd  1309  3bior2fd  1311  cadanOLD  1428  euor  2294  euor2  2296  eueq3  3112  unineq  3577  ifor  3813  difprsnss  3984  disjprg  4263  disjxun  4265  opthwiener  4565  opthprc  4857  swoord1  7091  brwdomn0  7731  fpwwe2lem13  8755  ne0gt0  9425  xrinfmss  11217  sumsplit  13176  sadadd2lem2  13586  coprm  13726  vdwlem11  13992  lvecvscan  17001  lvecvscan2  17002  mplcoe1  17351  mplcoe2  17353  maducoeval2  18150  xrsxmet  20086  itg2split  20927  plydiveu  21505  quotcan  21516  coseq1  21725  angrtmuld  21945  leibpilem2  22077  leibpi  22078  wilthlem2  22148  tgldimor  22693  tgcolg  22723  axcontlem7  22895  nb3graprlem2  23039  eupath2lem2  23278  eupath2lem3  23279  nmlnogt0  23876  hvmulcan  24153  hvmulcan2  24154  disjunsn  25616  xrdifh  25748  itgaddnclem2  28122  pr1eqbg  29795  elpadd0  32890
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 179  df-or 363
  Copyright terms: Public domain W3C validator