Theorem biorf 942

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  biortn  943  biorfi  944  pm5.55  956  pm5.75  1036  3bior1fd  1483  3bior2fd  1485  norasslem3  1543  euor  2615  euorv  2616  euor2  2617  eueq3  3659  unineq  4223  ifor  4516  difprsnss  4739  eqsn  4767  pr1eqbg  4795  disjprg  5075  disjxun  5077  opthwiener  5462  swoord1  8673  brwdomn0  9481  fpwwe2lem12  10563  ne0gt0  11249  xrinfmss  13260  sumsplit  15728  sadadd2lem2  16417  coprm  16679  vdwlem11  16960  lvecvscan  21111  lvecvscan2  21112  mplcoe1  22020  mplcoe5  22023  maducoeval2  22630  xrsxmet  24800  itg2split  25741  plydiveu  26289  quotcan  26300  coseq1  26514  angrtmuld  26797  leibpilem2  26930  leibpi  26931  wilthlem2  27057  tgldimor  28595  tgcolg  28647  axcontlem7  29064  elntg2  29079  nb3grprlem2  29475  eupth2lem2  30314  eupth2lem3lem6  30328  nmlnogt0  30893  hvmulcan  31168  hvmulcan2  31169  rmounid  32589  disjunsn  32690  xrdifh  32879  bj-snmoore  37478  nlpineqsn  37777  wl-ifp-ncond1  37833  itgaddnclem2  38053  biorfd  38611  elpadd0  40308  fsuppind  43047  or3or  44474