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

Step	Hyp	Ref	Expression
1		olc 857	. 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓))
2		orel1 875	. 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))
3	1, 2	impbid2 216	1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))

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