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  1537  euor  2608  euorv  2609  euor2  2610  eueq3  3666  unineq  4237  ifor  4531  difprsnss  4752  eqsn  4782  pr1eqbg  4810  disjprg  5091  disjxun  5093  opthwiener  5459  swoord1  8662  brwdomn0  9464  fpwwe2lem12  10542  ne0gt0  11227  xrinfmss  13213  sumsplit  15679  sadadd2lem2  16365  coprm  16626  vdwlem11  16907  lvecvscan  21052  lvecvscan2  21053  mplcoe1  21975  mplcoe5  21978  maducoeval2  22558  xrsxmet  24728  itg2split  25680  plydiveu  26236  quotcan  26247  coseq1  26464  angrtmuld  26748  leibpilem2  26881  leibpi  26882  wilthlem2  27009  tgldimor  28483  tgcolg  28535  axcontlem7  28952  elntg2  28967  nb3grprlem2  29363  eupth2lem2  30203  eupth2lem3lem6  30217  nmlnogt0  30781  hvmulcan  31056  hvmulcan2  31057  rmounid  32478  disjunsn  32578  xrdifh  32769  bj-snmoore  37180  nlpineqsn  37475  wl-ifp-ncond1  37531  itgaddnclem2  37742  biorfd  38295  elpadd0  39931  fsuppind  42711  or3or  44143