Theorem biorf 934

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  biortn  935  pm5.55  946  pm5.75  1026  3bior1fd  1474  3bior2fd  1476  norasslem3  1536  euor  2611  euorv  2612  euor2  2613  eueq3  3656  unineq  4223  ifor  4526  difprsnss  4745  eqsn  4775  pr1eqbg  4800  disjprgw  5084  disjprg  5085  disjxun  5087  opthwiener  5452  opthprc  5676  swoord1  8592  brwdomn0  9418  fpwwe2lem12  10491  ne0gt0  11173  xrinfmss  13137  sumsplit  15571  sadadd2lem2  16248  coprm  16505  vdwlem11  16781  lvecvscan  20471  lvecvscan2  20472  mplcoe1  21336  mplcoe5  21339  maducoeval2  21887  xrsxmet  24070  itg2split  25012  plydiveu  25556  quotcan  25567  coseq1  25779  angrtmuld  26056  leibpilem2  26189  leibpi  26190  wilthlem2  26316  tgldimor  27093  tgcolg  27145  axcontlem7  27568  elntg2  27583  nb3grprlem2  27978  eupth2lem2  28812  eupth2lem3lem6  28826  nmlnogt0  29388  hvmulcan  29663  hvmulcan2  29664  rmounid  31072  disjunsn  31161  xrdifh  31329  frxp2  34017  bj-biorfi  34856  bj-snmoore  35382  nlpineqsn  35677  wl-ifp-ncond1  35733  itgaddnclem2  35934  biorfd  36486  elpadd0  38070  fsuppind  40529  or3or  41941