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  1476  3bior2fd  1478  norasslem3  1535  euor  2609  euorv  2610  euor2  2611  eueq3  3692  unineq  4261  ifor  4553  difprsnss  4773  eqsn  4803  pr1eqbg  4831  disjprg  5113  disjxun  5115  opthwiener  5487  swoord1  8746  brwdomn0  9576  fpwwe2lem12  10649  ne0gt0  11333  xrinfmss  13319  sumsplit  15773  sadadd2lem2  16456  coprm  16717  vdwlem11  16998  lvecvscan  21059  lvecvscan2  21060  mplcoe1  21982  mplcoe5  21985  maducoeval2  22565  xrsxmet  24736  itg2split  25689  plydiveu  26245  quotcan  26256  coseq1  26472  angrtmuld  26756  leibpilem2  26889  leibpi  26890  wilthlem2  27017  tgldimor  28415  tgcolg  28467  axcontlem7  28883  elntg2  28898  nb3grprlem2  29294  eupth2lem2  30134  eupth2lem3lem6  30148  nmlnogt0  30712  hvmulcan  30987  hvmulcan2  30988  rmounid  32410  disjunsn  32509  xrdifh  32694  bj-snmoore  37060  nlpineqsn  37355  wl-ifp-ncond1  37411  itgaddnclem2  37632  biorfd  38178  elpadd0  39757  fsuppind  42545  or3or  43979