Theorem biorf 935

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

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

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 847

This theorem is referenced by:  biortn  936  biorfi  937  pm5.55  949  pm5.75  1029  3bior1fd  1475  3bior2fd  1477  norasslem3  1533  euor  2614  euorv  2615  euor2  2616  eueq3  3733  unineq  4307  ifor  4602  difprsnss  4824  eqsn  4854  pr1eqbg  4881  disjprg  5162  disjxun  5164  opthwiener  5533  swoord1  8795  brwdomn0  9638  fpwwe2lem12  10711  ne0gt0  11395  xrinfmss  13372  sumsplit  15816  sadadd2lem2  16496  coprm  16758  vdwlem11  17038  lvecvscan  21136  lvecvscan2  21137  mplcoe1  22078  mplcoe5  22081  maducoeval2  22667  xrsxmet  24850  itg2split  25804  plydiveu  26358  quotcan  26369  coseq1  26585  angrtmuld  26869  leibpilem2  27002  leibpi  27003  wilthlem2  27130  tgldimor  28528  tgcolg  28580  axcontlem7  29003  elntg2  29018  nb3grprlem2  29416  eupth2lem2  30251  eupth2lem3lem6  30265  nmlnogt0  30829  hvmulcan  31104  hvmulcan2  31105  rmounid  32523  disjunsn  32616  xrdifh  32785  bj-snmoore  37079  nlpineqsn  37374  wl-ifp-ncond1  37430  itgaddnclem2  37639  biorfd  38186  elpadd0  39766  fsuppind  42545  or3or  43985