Theorem biorf 947

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  biortn  948  biorfi  949  pm5.55  961  pm5.75  1041  3bior1fd  1495  3bior2fd  1497  norasslem3  1555  euor  2637  euorv  2638  euor2  2639  eueq3  3672  unineq  4238  ifor  4532  difprsnss  4756  eqsn  4784  pr1eqbg  4812  disjprg  5093  disjxun  5095  opthwiener  5480  swoord1  8704  brwdomn0  9510  fpwwe2lem12  10593  ne0gt0  11281  xrinfmss  13306  sumsplit  15785  sadadd2lem2  16474  coprm  16736  vdwlem11  17017  lvecvscan  21168  lvecvscan2  21169  mplcoe1  22077  mplcoe5  22080  maducoeval2  22687  xrsxmet  24857  itg2split  25798  plydiveu  26349  quotcan  26360  coseq1  26577  angrtmuld  26860  leibpilem2  26993  leibpi  26994  wilthlem2  27120  tgldimor  28658  tgcolg  28710  axcontlem7  29127  elntg2  29142  nb3grprlem2  29538  eupth2lem2  30377  eupth2lem3lem6  30391  nmlnogt0  30956  hvmulcan  31231  hvmulcan2  31232  rmounid  32652  disjunsn  32753  xrdifh  32942  bj-snmoore  37563  nlpineqsn  37862  wl-ifp-ncond1  37918  itgaddnclem2  38138  biorfd  38696  elpadd0  40393  fsuppind  43132  or3or  44559