Theorem biorf 933

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 843

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 206  df-or 844

This theorem is referenced by:  biortn  934  pm5.55  945  pm5.75  1025  3bior1fd  1473  3bior2fd  1475  norasslem3  1534  euor  2613  euorv  2614  euor2  2615  eueq3  3641  unineq  4208  ifor  4510  difprsnss  4729  eqsn  4759  pr1eqbg  4784  dfopif  4797  disjprgw  5065  disjprg  5066  disjxun  5068  opthwiener  5422  opthprc  5642  swoord1  8487  brwdomn0  9258  fpwwe2lem12  10329  ne0gt0  11010  xrinfmss  12973  sumsplit  15408  sadadd2lem2  16085  coprm  16344  vdwlem11  16620  lvecvscan  20288  lvecvscan2  20289  mplcoe1  21148  mplcoe5  21151  maducoeval2  21697  xrsxmet  23878  itg2split  24819  plydiveu  25363  quotcan  25374  coseq1  25586  angrtmuld  25863  leibpilem2  25996  leibpi  25997  wilthlem2  26123  tgldimor  26767  tgcolg  26819  axcontlem7  27241  elntg2  27256  nb3grprlem2  27651  eupth2lem2  28484  eupth2lem3lem6  28498  nmlnogt0  29060  hvmulcan  29335  hvmulcan2  29336  rmounid  30744  disjunsn  30834  xrdifh  31003  frxp2  33718  bj-biorfi  34692  bj-snmoore  35211  nlpineqsn  35506  wl-ifp-ncond1  35562  itgaddnclem2  35763  elpadd0  37750  fsuppind  40202  or3or  41520