Theorem biorf 949

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  biortn  950  biorfi  951  pm5.55  963  pm5.75  1044  3bior1fd  1503  3bior2fd  1505  norasslem3  1563  euor  2645  euorv  2646  euor2  2647  eueq3  3683  unineq  4249  ifor  4547  difprsnss  4771  eqsn  4799  pr1eqbg  4826  disjprg  5109  disjxun  5111  opthwiener  5500  swoord1  8729  brwdomn0  9533  fpwwe2lem12  10629  ne0gt0  11317  xrinfmss  13338  sumsplit  15821  sadadd2lem2  16510  coprm  16772  vdwlem11  17053  lvecvscan  21215  lvecvscan2  21216  mplcoe1  22159  mplcoe5  22162  maducoeval2  22768  xrsxmet  24938  itg2split  25879  plydiveu  26430  quotcan  26441  coseq1  26658  angrtmuld  26941  leibpilem2  27074  leibpi  27075  wilthlem2  27201  tgldimor  28739  tgcolg  28791  axcontlem7  29263  elntg2  29278  nb3grprlem2  29674  eupth2lem2  30513  eupth2lem3lem6  30527  nmlnogt0  31092  hvmulcan  31367  hvmulcan2  31368  rmounid  32784  disjunsn  32882  xrdifh  33068  bj-snmoore  37680  nlpineqsn  37979  wl-ifp-ncond1  38035  itgaddnclem2  38255  biorfd  38813  elpadd0  40510  fsuppind  43251  or3or  44678