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  2605  euorv  2606  euor2  2607  eueq3  3685  unineq  4254  ifor  4546  difprsnss  4766  eqsn  4796  pr1eqbg  4824  disjprg  5106  disjxun  5108  opthwiener  5477  swoord1  8706  brwdomn0  9529  fpwwe2lem12  10602  ne0gt0  11286  xrinfmss  13277  sumsplit  15741  sadadd2lem2  16427  coprm  16688  vdwlem11  16969  lvecvscan  21028  lvecvscan2  21029  mplcoe1  21951  mplcoe5  21954  maducoeval2  22534  xrsxmet  24705  itg2split  25657  plydiveu  26213  quotcan  26224  coseq1  26441  angrtmuld  26725  leibpilem2  26858  leibpi  26859  wilthlem2  26986  tgldimor  28436  tgcolg  28488  axcontlem7  28904  elntg2  28919  nb3grprlem2  29315  eupth2lem2  30155  eupth2lem3lem6  30169  nmlnogt0  30733  hvmulcan  31008  hvmulcan2  31009  rmounid  32431  disjunsn  32530  xrdifh  32710  bj-snmoore  37108  nlpineqsn  37403  wl-ifp-ncond1  37459  itgaddnclem2  37680  biorfd  38226  elpadd0  39810  fsuppind  42585  or3or  44019