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  1536  euor  2604  euorv  2605  euor2  2606  eueq3  3682  unineq  4251  ifor  4543  difprsnss  4763  eqsn  4793  pr1eqbg  4821  disjprg  5103  disjxun  5105  opthwiener  5474  swoord1  8703  brwdomn0  9522  fpwwe2lem12  10595  ne0gt0  11279  xrinfmss  13270  sumsplit  15734  sadadd2lem2  16420  coprm  16681  vdwlem11  16962  lvecvscan  21021  lvecvscan2  21022  mplcoe1  21944  mplcoe5  21947  maducoeval2  22527  xrsxmet  24698  itg2split  25650  plydiveu  26206  quotcan  26217  coseq1  26434  angrtmuld  26718  leibpilem2  26851  leibpi  26852  wilthlem2  26979  tgldimor  28429  tgcolg  28481  axcontlem7  28897  elntg2  28912  nb3grprlem2  29308  eupth2lem2  30148  eupth2lem3lem6  30162  nmlnogt0  30726  hvmulcan  31001  hvmulcan2  31002  rmounid  32424  disjunsn  32523  xrdifh  32703  bj-snmoore  37101  nlpineqsn  37396  wl-ifp-ncond1  37452  itgaddnclem2  37673  biorfd  38219  elpadd0  39803  fsuppind  42578  or3or  44012