Theorem biorf 951

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∨ wo 865

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 198  df-or 866

This theorem is referenced by:  biortn  952  pm5.55  962  pm5.61  1014  pm5.75  1044  3bior1fd  1592  3bior2fd  1594  euor  2675  euor2  2677  eueq3  3579  unineq  4079  ifor  4331  difprsnss  4520  eqsn  4550  pr1eqbg  4577  disjprg  4840  disjxun  4842  opthwiener  5169  opthprc  5367  swoord1  8010  brwdomn0  8713  fpwwe2lem13  9749  ne0gt0  10427  xrinfmss  12358  sumsplit  14722  sadadd2lem2  15391  coprm  15640  vdwlem11  15912  lvecvscan  19318  lvecvscan2  19319  mplcoe1  19674  mplcoe5  19677  maducoeval2  20657  xrsxmet  22825  itg2split  23730  plydiveu  24267  quotcan  24278  coseq1  24489  angrtmuld  24752  leibpilem2  24882  leibpi  24883  wilthlem2  25009  tgldimor  25611  tgcolg  25663  axcontlem7  26064  nb3grprlem2  26499  eupth2lem2  27392  eupth2lem3lem6  27406  nmlnogt0  27980  hvmulcan  28257  hvmulcan2  28258  disjunsn  29732  xrdifh  29869  bj-biorfi  32883  bj-snmoore  33379  itgaddnclem2  33781  elpadd0  35589  or3or  38819