Theorem biorf 936

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 868	. 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓))
2		orel1 888	. 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓))
3	1, 2	impbid2 226	1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  biortn  937  biorfi  938  pm5.55  950  pm5.75  1030  3bior1fd  1477  3bior2fd  1479  norasslem3  1536  euor  2604  euorv  2605  euor2  2606  eueq3  3673  unineq  4241  ifor  4533  difprsnss  4753  eqsn  4783  pr1eqbg  4811  disjprg  5091  disjxun  5093  opthwiener  5461  swoord1  8664  brwdomn0  9480  fpwwe2lem12  10555  ne0gt0  11239  xrinfmss  13230  sumsplit  15693  sadadd2lem2  16379  coprm  16640  vdwlem11  16921  lvecvscan  21036  lvecvscan2  21037  mplcoe1  21960  mplcoe5  21963  maducoeval2  22543  xrsxmet  24714  itg2split  25666  plydiveu  26222  quotcan  26233  coseq1  26450  angrtmuld  26734  leibpilem2  26867  leibpi  26868  wilthlem2  26995  tgldimor  28465  tgcolg  28517  axcontlem7  28933  elntg2  28948  nb3grprlem2  29344  eupth2lem2  30181  eupth2lem3lem6  30195  nmlnogt0  30759  hvmulcan  31034  hvmulcan2  31035  rmounid  32457  disjunsn  32556  xrdifh  32736  bj-snmoore  37089  nlpineqsn  37384  wl-ifp-ncond1  37440  itgaddnclem2  37661  biorfd  38207  elpadd0  39791  fsuppind  42566  or3or  43999