Theorem biorf 936

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  biortn  937  biorfi  938  pm5.55  950  pm5.75  1030  3bior1fd  1474  3bior2fd  1476  norasslem3  1532  euor  2608  euorv  2609  euor2  2610  eueq3  3719  unineq  4293  ifor  4584  difprsnss  4803  eqsn  4833  pr1eqbg  4861  disjprg  5143  disjxun  5145  opthwiener  5523  swoord1  8775  brwdomn0  9606  fpwwe2lem12  10679  ne0gt0  11363  xrinfmss  13348  sumsplit  15800  sadadd2lem2  16483  coprm  16744  vdwlem11  17024  lvecvscan  21130  lvecvscan2  21131  mplcoe1  22072  mplcoe5  22075  maducoeval2  22661  xrsxmet  24844  itg2split  25798  plydiveu  26354  quotcan  26365  coseq1  26581  angrtmuld  26865  leibpilem2  26998  leibpi  26999  wilthlem2  27126  tgldimor  28524  tgcolg  28576  axcontlem7  28999  elntg2  29014  nb3grprlem2  29412  eupth2lem2  30247  eupth2lem3lem6  30261  nmlnogt0  30825  hvmulcan  31100  hvmulcan2  31101  rmounid  32522  disjunsn  32613  xrdifh  32788  bj-snmoore  37095  nlpineqsn  37390  wl-ifp-ncond1  37446  itgaddnclem2  37665  biorfd  38211  elpadd0  39791  fsuppind  42576  or3or  44012