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

Theorem biorf 418
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 397 . 2 (𝜓 → (𝜑𝜓))
2 orel1 395 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 214 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381
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 195  df-or 383
This theorem is referenced by:  biortn  419  pm5.61  744  pm5.55  936  pm5.75  973  3bior1fd  1429  3bior2fd  1431  euor  2499  euor2  2501  eueq3  3347  unineq  3835  ifor  4084  difprsnss  4269  eqsn  4298  disjprg  4572  disjxun  4575  opthwiener  4892  opthprc  5079  swoord1  7637  brwdomn0  8334  fpwwe2lem13  9320  ne0gt0  9993  xrinfmss  11968  sumsplit  14287  sadadd2lem2  14956  coprm  15207  vdwlem11  15479  lvecvscan  18878  lvecvscan2  18879  mplcoe1  19232  mplcoe5  19235  maducoeval2  20207  xrsxmet  22352  itg2split  23239  plydiveu  23774  quotcan  23785  coseq1  23995  angrtmuld  24255  leibpilem2  24385  leibpi  24386  wilthlem2  24512  tgldimor  25114  tgcolg  25167  axcontlem7  25568  nb3graprlem2  25747  eupath2lem2  26271  eupath2lem3  26272  nmlnogt0  26842  hvmulcan  27119  hvmulcan2  27120  disjunsn  28595  xrdifh  28738  bj-biorfi  31547  itgaddnclem2  32442  elpadd0  33916  or3or  37142  pr1eqbg  40118  nb3grprlem2  40611  eupth2lem2  41389  eupth2lem3lem6  41403
  Copyright terms: Public domain W3C validator