MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biorf 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

Proof of Theorem biorf
StepHypRef Expression
1 olc 384 . 2
2 orel1 382 . 2
31, 2impbid2 204 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368
This theorem is referenced by:  biortn  406  pm5.61  712  pm5.55  897  3bior1fd  1334  3bior2fd  1336  euor  2331  euor2  2333  eueq3  3274  unineq  3747  ifor  3988  difprsnss  4165  disjprg  4448  disjxun  4450  opthwiener  4754  opthprc  5052  swoord1  7359  brwdomn0  8016  fpwwe2lem13  9041  ne0gt0  9710  xrinfmss  11530  sumsplit  13583  sadadd2lem2  14100  coprm  14241  vdwlem11  14509  lvecvscan  17757  lvecvscan2  17758  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  maducoeval2  19142  xrsxmet  21314  itg2split  22156  plydiveu  22694  quotcan  22705  coseq1  22915  angrtmuld  23140  leibpilem2  23272  leibpi  23273  wilthlem2  23343  tgldimor  23893  tgcolg  23941  axcontlem7  24273  nb3graprlem2  24452  eupath2lem2  24978  eupath2lem3  24979  nmlnogt0  25712  hvmulcan  25989  hvmulcan2  25990  disjunsn  27453  xrdifh  27591  itgaddnclem2  30074  pr1eqbg  32297  bj-biorfi  34172  elpadd0  35533
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
  Copyright terms: Public domain W3C validator