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

Theorem biorf 922
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 857 . 2 (𝜓 → (𝜑𝜓))
2 orel1 875 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 216 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 836
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 197  df-or 837
This theorem is referenced by:  biortn  923  pm5.55  933  pm5.61  985  pm5.75  1015  3bior1fd  1586  3bior2fd  1588  euor  2661  euor2  2663  eueq3  3533  unineq  4026  ifor  4274  difprsnss  4465  eqsn  4495  pr1eqbg  4521  disjprg  4782  disjxun  4784  opthwiener  5107  opthprc  5307  swoord1  7927  brwdomn0  8630  fpwwe2lem13  9666  ne0gt0  10344  xrinfmss  12345  sumsplit  14707  sadadd2lem2  15380  coprm  15630  vdwlem11  15902  lvecvscan  19324  lvecvscan2  19325  mplcoe1  19680  mplcoe5  19683  maducoeval2  20664  xrsxmet  22832  itg2split  23736  plydiveu  24273  quotcan  24284  coseq1  24495  angrtmuld  24759  leibpilem2  24889  leibpi  24890  wilthlem2  25016  tgldimor  25618  tgcolg  25670  axcontlem7  26071  nb3grprlem2  26506  eupth2lem2  27399  eupth2lem3lem6  27413  nmlnogt0  27992  hvmulcan  28269  hvmulcan2  28270  disjunsn  29745  xrdifh  29882  bj-biorfi  32905  bj-snmoore  33400  itgaddnclem2  33801  elpadd0  35617  or3or  38845
  Copyright terms: Public domain W3C validator