Theorem biorf 934

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

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

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 845

This theorem is referenced by:  biortn  935  pm5.55  946  pm5.75  1026  3bior1fd  1474  3bior2fd  1476  norasslem3  1534  euor  2613  euorv  2614  euor2  2615  eueq3  3646  unineq  4211  ifor  4513  difprsnss  4732  eqsn  4762  pr1eqbg  4787  dfopif  4800  disjprgw  5069  disjprg  5070  disjxun  5072  opthwiener  5428  opthprc  5651  swoord1  8529  brwdomn0  9328  fpwwe2lem12  10398  ne0gt0  11080  xrinfmss  13044  sumsplit  15480  sadadd2lem2  16157  coprm  16416  vdwlem11  16692  lvecvscan  20373  lvecvscan2  20374  mplcoe1  21238  mplcoe5  21241  maducoeval2  21789  xrsxmet  23972  itg2split  24914  plydiveu  25458  quotcan  25469  coseq1  25681  angrtmuld  25958  leibpilem2  26091  leibpi  26092  wilthlem2  26218  tgldimor  26863  tgcolg  26915  axcontlem7  27338  elntg2  27353  nb3grprlem2  27748  eupth2lem2  28583  eupth2lem3lem6  28597  nmlnogt0  29159  hvmulcan  29434  hvmulcan2  29435  rmounid  30843  disjunsn  30933  xrdifh  31101  frxp2  33791  bj-biorfi  34765  bj-snmoore  35284  nlpineqsn  35579  wl-ifp-ncond1  35635  itgaddnclem2  35836  elpadd0  37823  fsuppind  40279  or3or  41631