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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  biortn  935  pm5.55  946  pm5.75  1026  3bior1fd  1472  3bior2fd  1474  norasslem3  1533  euor  2672  euorv  2673  euor2  2674  eueq3  3650  unineq  4204  ifor  4477  difprsnss  4692  eqsn  4722  pr1eqbg  4747  disjprgw  5025  disjprg  5026  disjxun  5028  opthwiener  5369  opthprc  5580  swoord1  8303  brwdomn0  9017  fpwwe2lem13  10053  ne0gt0  10734  xrinfmss  12691  sumsplit  15115  sadadd2lem2  15789  coprm  16045  vdwlem11  16317  lvecvscan  19876  lvecvscan2  19877  mplcoe1  20705  mplcoe5  20708  maducoeval2  21245  xrsxmet  23414  itg2split  24353  plydiveu  24894  quotcan  24905  coseq1  25117  angrtmuld  25394  leibpilem2  25527  leibpi  25528  wilthlem2  25654  tgldimor  26296  tgcolg  26348  axcontlem7  26764  elntg2  26779  nb3grprlem2  27171  eupth2lem2  28004  eupth2lem3lem6  28018  nmlnogt0  28580  hvmulcan  28855  hvmulcan2  28856  rmounid  30266  disjunsn  30357  xrdifh  30529  bj-biorfi  34030  bj-snmoore  34528  nlpineqsn  34825  wl-ifp-ncond1  34881  itgaddnclem2  35116  elpadd0  37105  fsuppind  39456  or3or  40724