Theorem biorf 420

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383

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 197  df-or 385

This theorem is referenced by:  biortn  421  pm5.61  749  pm5.55  939  pm5.75  978  3bior1fd  1438  3bior2fd  1440  euor  2512  euor2  2514  eueq3  3381  unineq  3877  ifor  4135  difprsnss  4329  eqsn  4361  pr1eqbg  4390  disjprg  4648  disjxun  4651  opthwiener  4976  opthprc  5167  swoord1  7773  brwdomn0  8474  fpwwe2lem13  9464  ne0gt0  10142  xrinfmss  12140  sumsplit  14499  sadadd2lem2  15172  coprm  15423  vdwlem11  15695  lvecvscan  19111  lvecvscan2  19112  mplcoe1  19465  mplcoe5  19468  maducoeval2  20446  xrsxmet  22612  itg2split  23516  plydiveu  24053  quotcan  24064  coseq1  24274  angrtmuld  24538  leibpilem2  24668  leibpi  24669  wilthlem2  24795  tgldimor  25397  tgcolg  25449  axcontlem7  25850  nb3grprlem2  26283  eupth2lem2  27079  eupth2lem3lem6  27093  nmlnogt0  27652  hvmulcan  27929  hvmulcan2  27930  disjunsn  29407  xrdifh  29542  bj-biorfi  32568  bj-snmoore  33068  itgaddnclem2  33469  elpadd0  35095  or3or  38319