Theorem biorf 950

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  biortn  951  biorfi  952  pm5.55  963  pm5.75  1046  3bior1fd  1506  3bior2fd  1508  norasslem3  1566  euor  2641  euorv  2642  euor2  2643  eueq3  3676  unineq  4241  ifor  4544  difprsnss  4769  eqsn  4797  pr1eqbg  4824  disjprg  5107  disjxun  5109  opthwiener  5499  swoord1  8729  brwdomn0  9534  fpwwe2lem12  10638  ne0gt0  11326  xrinfmss  13348  sumsplit  15838  sadadd2lem2  16526  coprm  16788  vdwlem11  17069  lvecvscan  21265  lvecvscan2  21266  mplcoe1  22218  mplcoe5  22221  maducoeval2  22827  xrsxmet  24998  itg2split  25939  plydiveu  26490  quotcan  26501  coseq1  26721  angrtmuld  27004  leibpilem2  27137  leibpi  27138  wilthlem2  27264  tgldimor  28802  tgcolg  28854  dfprlng2  29228  axcontlem7  29351  elntg2  29366  nb3grprlem2  29765  eupth2lem2  30617  eupth2lem3lem6  30631  nmlnogt0  31196  hvmulcan  31471  hvmulcan2  31472  rmounid  32888  disjunsn  32986  xrdifh  33171  bj-snmoore  37788  nlpineqsn  38087  wl-ifp-ncond1  38143  itgaddnclem2  38363  biorfd  38919  elpadd0  40616  fsuppind  43355  or3or  44782