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  4544  difprsnss  4768  eqsn  4796  pr1eqbg  4823  disjprg  5106  disjxun  5108  opthwiener  5495  swoord1  8723  brwdomn0  9527  fpwwe2lem12  10623  ne0gt0  11311  xrinfmss  13332  sumsplit  15815  sadadd2lem2  16504  coprm  16766  vdwlem11  17047  lvecvscan  21209  lvecvscan2  21210  mplcoe1  22153  mplcoe5  22156  maducoeval2  22762  xrsxmet  24932  itg2split  25873  plydiveu  26424  quotcan  26435  coseq1  26652  angrtmuld  26935  leibpilem2  27068  leibpi  27069  wilthlem2  27195  tgldimor  28733  tgcolg  28785  axcontlem7  29257  elntg2  29272  nb3grprlem2  29668  eupth2lem2  30507  eupth2lem3lem6  30521  nmlnogt0  31086  hvmulcan  31361  hvmulcan2  31362  rmounid  32778  disjunsn  32876  xrdifh  33062  bj-snmoore  37638  nlpineqsn  37937  wl-ifp-ncond1  37993  itgaddnclem2  38213  biorfd  38771  elpadd0  40468  fsuppind  43207  or3or  44634