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

Theorem biorf 930
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 862 . 2 (𝜓 → (𝜑𝜓))
2 orel1 882 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 227 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wo 841
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 208  df-or 842
This theorem is referenced by:  biortn  931  pm5.55  942  pm5.75  1022  3bior1fd  1466  3bior2fd  1468  norasslem3  1523  euor  2688  euorv  2689  euor2  2690  eueq3  3699  unineq  4251  ifor  4515  difprsnss  4724  eqsn  4754  pr1eqbg  4779  disjprgw  5052  disjprg  5053  disjxun  5055  opthwiener  5395  opthprc  5609  swoord1  8309  brwdomn0  9021  fpwwe2lem13  10052  ne0gt0  10733  xrinfmss  12691  sumsplit  15111  sadadd2lem2  15787  coprm  16043  vdwlem11  16315  lvecvscan  19812  lvecvscan2  19813  mplcoe1  20174  mplcoe5  20177  maducoeval2  21177  xrsxmet  23344  itg2split  24277  plydiveu  24814  quotcan  24825  coseq1  25037  angrtmuld  25313  leibpilem2  25446  leibpi  25447  wilthlem2  25573  tgldimor  26215  tgcolg  26267  axcontlem7  26683  elntg2  26698  nb3grprlem2  27090  eupth2lem2  27925  eupth2lem3lem6  27939  nmlnogt0  28501  hvmulcan  28776  hvmulcan2  28777  rmounid  30186  disjunsn  30272  xrdifh  30429  bj-biorfi  33814  bj-snmoore  34299  nlpineqsn  34571  itgaddnclem2  34832  elpadd0  36825  or3or  40249
  Copyright terms: Public domain W3C validator