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  1536  euor  2610  euorv  2611  euor2  2612  eueq3  3694  unineq  4263  ifor  4555  difprsnss  4775  eqsn  4805  pr1eqbg  4833  disjprg  5115  disjxun  5117  opthwiener  5489  swoord1  8751  brwdomn0  9583  fpwwe2lem12  10656  ne0gt0  11340  xrinfmss  13326  sumsplit  15784  sadadd2lem2  16469  coprm  16730  vdwlem11  17011  lvecvscan  21072  lvecvscan2  21073  mplcoe1  21995  mplcoe5  21998  maducoeval2  22578  xrsxmet  24749  itg2split  25702  plydiveu  26258  quotcan  26269  coseq1  26486  angrtmuld  26770  leibpilem2  26903  leibpi  26904  wilthlem2  27031  tgldimor  28481  tgcolg  28533  axcontlem7  28949  elntg2  28964  nb3grprlem2  29360  eupth2lem2  30200  eupth2lem3lem6  30214  nmlnogt0  30778  hvmulcan  31053  hvmulcan2  31054  rmounid  32476  disjunsn  32575  xrdifh  32757  bj-snmoore  37131  nlpineqsn  37426  wl-ifp-ncond1  37482  itgaddnclem2  37703  biorfd  38249  elpadd0  39828  fsuppind  42613  or3or  44047