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

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

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 846

This theorem is referenced by:  biortn  935  pm5.55  946  pm5.75  1026  3bior1fd  1471  3bior2fd  1473  norasslem3  1529  euor  2599  euorv  2600  euor2  2601  eueq3  3703  unineq  4276  ifor  4584  difprsnss  4804  eqsn  4834  pr1eqbg  4859  disjprgw  5144  disjprg  5145  disjxun  5147  opthwiener  5516  opthprc  5742  frxp2  8149  swoord1  8756  brwdomn0  9594  fpwwe2lem12  10667  ne0gt0  11351  xrinfmss  13324  sumsplit  15750  sadadd2lem2  16428  coprm  16685  vdwlem11  16963  lvecvscan  21011  lvecvscan2  21012  mplcoe1  21997  mplcoe5  22000  maducoeval2  22586  xrsxmet  24769  itg2split  25723  plydiveu  26278  quotcan  26289  coseq1  26504  angrtmuld  26785  leibpilem2  26918  leibpi  26919  wilthlem2  27046  tgldimor  28378  tgcolg  28430  axcontlem7  28853  elntg2  28868  nb3grprlem2  29266  eupth2lem2  30101  eupth2lem3lem6  30115  nmlnogt0  30679  hvmulcan  30954  hvmulcan2  30955  rmounid  32371  disjunsn  32463  xrdifh  32630  bj-biorfi  36188  bj-snmoore  36720  nlpineqsn  37015  wl-ifp-ncond1  37071  itgaddnclem2  37280  biorfd  37829  elpadd0  39409  fsuppind  41955  or3or  43592