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 215 1 𝜑 → (𝜓 ↔ (𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ 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 196  df-or 384 This theorem is referenced by:  biortn  420  pm5.61  745  pm5.55  937  pm5.75  974  3bior1fd  1430  3bior2fd  1432  euor  2500  euor2  2502  eueq3  3348  unineq  3836  ifor  4085  difprsnss  4270  eqsn  4301  disjprg  4578  disjxun  4581  opthwiener  4901  opthprc  5089  swoord1  7660  brwdomn0  8357  fpwwe2lem13  9343  ne0gt0  10021  xrinfmss  12012  sumsplit  14341  sadadd2lem2  15010  coprm  15261  vdwlem11  15533  lvecvscan  18932  lvecvscan2  18933  mplcoe1  19286  mplcoe5  19289  maducoeval2  20265  xrsxmet  22420  itg2split  23322  plydiveu  23857  quotcan  23868  coseq1  24078  angrtmuld  24338  leibpilem2  24468  leibpi  24469  wilthlem2  24595  tgldimor  25197  tgcolg  25249  axcontlem7  25650  nb3graprlem2  25981  eupath2lem2  26505  eupath2lem3  26506  nmlnogt0  27036  hvmulcan  27313  hvmulcan2  27314  disjunsn  28789  xrdifh  28932  bj-biorfi  31741  itgaddnclem2  32639  elpadd0  34113  or3or  37339  pr1eqbg  40313  nb3grprlem2  40609  eupth2lem2  41387  eupth2lem3lem6  41401
 Copyright terms: Public domain W3C validator