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

Theorem biorf 419
 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 398 . 2 (𝜓 → (𝜑𝜓))
2 orel1 396 . 2 𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 216 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382 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 384 This theorem is referenced by:  biortn  420  pm5.61  749  pm5.55  957  pm5.75  998  3bior1fd  1478  3bior2fd  1480  euor  2541  euor2  2543  eueq3  3414  unineq  3910  ifor  4168  difprsnss  4361  eqsn  4393  pr1eqbg  4421  disjprg  4680  disjxun  4683  opthwiener  5005  opthprc  5201  swoord1  7818  brwdomn0  8515  fpwwe2lem13  9502  ne0gt0  10180  xrinfmss  12178  sumsplit  14543  sadadd2lem2  15219  coprm  15470  vdwlem11  15742  lvecvscan  19159  lvecvscan2  19160  mplcoe1  19513  mplcoe5  19516  maducoeval2  20494  xrsxmet  22659  itg2split  23561  plydiveu  24098  quotcan  24109  coseq1  24319  angrtmuld  24583  leibpilem2  24713  leibpi  24714  wilthlem2  24840  tgldimor  25442  tgcolg  25494  axcontlem7  25895  nb3grprlem2  26327  eupth2lem2  27197  eupth2lem3lem6  27211  nmlnogt0  27780  hvmulcan  28057  hvmulcan2  28058  disjunsn  29533  xrdifh  29670  bj-biorfi  32693  bj-snmoore  33193  itgaddnclem2  33599  elpadd0  35413  or3or  38636
 Copyright terms: Public domain W3C validator