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  1477  3bior2fd  1479  norasslem3  1537  euor  2606  euorv  2607  euor2  2608  eueq3  3670  unineq  4238  ifor  4530  difprsnss  4751  eqsn  4781  pr1eqbg  4809  disjprg  5087  disjxun  5089  opthwiener  5454  swoord1  8654  brwdomn0  9455  fpwwe2lem12  10533  ne0gt0  11218  xrinfmss  13209  sumsplit  15675  sadadd2lem2  16361  coprm  16622  vdwlem11  16903  lvecvscan  21049  lvecvscan2  21050  mplcoe1  21973  mplcoe5  21976  maducoeval2  22556  xrsxmet  24726  itg2split  25678  plydiveu  26234  quotcan  26245  coseq1  26462  angrtmuld  26746  leibpilem2  26879  leibpi  26880  wilthlem2  27007  tgldimor  28481  tgcolg  28533  axcontlem7  28949  elntg2  28964  nb3grprlem2  29360  eupth2lem2  30197  eupth2lem3lem6  30211  nmlnogt0  30775  hvmulcan  31050  hvmulcan2  31051  rmounid  32472  disjunsn  32572  xrdifh  32761  bj-snmoore  37153  nlpineqsn  37448  wl-ifp-ncond1  37504  itgaddnclem2  37725  biorfd  38271  elpadd0  39854  fsuppind  42629  or3or  44062