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  892  3bior1fd  1325  3bior2fd  1327  cadanOLD  1435  euor  2319  euor2  2321  eueq3  3244  unineq  3714  ifor  3952  difprsnss  4126  disjprg  4405  disjxun  4407  opthwiener  4710  opthprc  5003  swoord1  7264  brwdomn0  7921  fpwwe2lem13  8946  ne0gt0  9616  xrinfmss  11411  sumsplit  13393  sadadd2lem2  13804  coprm  13944  vdwlem11  14210  lvecvscan  17368  lvecvscan2  17369  mplcoe1  17721  mplcoe5  17725  mplcoe2OLD  17727  maducoeval2  18714  xrsxmet  20785  itg2split  21627  plydiveu  22164  quotcan  22175  coseq1  22384  angrtmuld  22604  leibpilem2  22736  leibpi  22737  wilthlem2  22807  tgldimor  23357  tgcolg  23405  axcontlem7  23685  nb3graprlem2  23829  eupath2lem2  24068  eupath2lem3  24069  nmlnogt0  24666  hvmulcan  24943  hvmulcan2  24944  disjunsn  26404  xrdifh  26531  itgaddnclem2  28911  pr1eqbg  30998  bj-biorfi  32952  elpadd0  34304
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