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  2611  euorv  2612  euor2  2613  eueq3  3669  unineq  4240  ifor  4534  difprsnss  4755  eqsn  4785  pr1eqbg  4813  disjprg  5094  disjxun  5096  opthwiener  5462  swoord1  8667  brwdomn0  9474  fpwwe2lem12  10553  ne0gt0  11238  xrinfmss  13225  sumsplit  15691  sadadd2lem2  16377  coprm  16638  vdwlem11  16919  lvecvscan  21066  lvecvscan2  21067  mplcoe1  21992  mplcoe5  21995  maducoeval2  22584  xrsxmet  24754  itg2split  25706  plydiveu  26262  quotcan  26273  coseq1  26490  angrtmuld  26774  leibpilem2  26907  leibpi  26908  wilthlem2  27035  tgldimor  28574  tgcolg  28626  axcontlem7  29043  elntg2  29058  nb3grprlem2  29454  eupth2lem2  30294  eupth2lem3lem6  30308  nmlnogt0  30872  hvmulcan  31147  hvmulcan2  31148  rmounid  32569  disjunsn  32669  xrdifh  32860  bj-snmoore  37318  nlpineqsn  37613  wl-ifp-ncond1  37669  itgaddnclem2  37880  biorfd  38433  elpadd0  40069  fsuppind  42833  or3or  44264