Theorem biorf 921

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∨ wo 834

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 199  df-or 835

This theorem is referenced by:  biortn  922  pm5.55  932  pm5.61  984  pm5.75  1012  3bior1fd  1455  3bior2fd  1457  euor  2645  euorv  2646  euor2  2648  eueq3  3618  unineq  4144  ifor  4405  difprsnss  4611  eqsn  4641  pr1eqbg  4666  disjprg  4930  disjxun  4932  opthwiener  5264  opthprc  5470  swoord1  8126  brwdomn0  8834  fpwwe2lem13  9868  ne0gt0  10551  xrinfmss  12525  sumsplit  14989  sadadd2lem2  15665  coprm  15917  vdwlem11  16189  lvecvscan  19617  lvecvscan2  19618  mplcoe1  19971  mplcoe5  19974  maducoeval2  20968  xrsxmet  23135  itg2split  24068  plydiveu  24605  quotcan  24616  coseq1  24828  angrtmuld  25102  leibpilem2  25236  leibpi  25237  wilthlem2  25363  tgldimor  26005  tgcolg  26057  axcontlem7  26474  elntg2  26489  nb3grprlem2  26881  eupth2lem2  27764  eupth2lem3lem6  27778  nmlnogt0  28366  hvmulcan  28643  hvmulcan2  28644  disjunsn  30127  xrdifh  30279  bj-biorfi  33474  bj-snmoore  33956  nlpineqsn  34170  itgaddnclem2  34432  elpadd0  36430  or3or  39775