Theorem biorf 936

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

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

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 847

This theorem is referenced by:  biortn  937  pm5.55  948  pm5.75  1028  3bior1fd  1476  3bior2fd  1478  norasslem3  1538  euor  2608  euorv  2609  euor2  2610  eueq3  3708  unineq  4278  ifor  4583  difprsnss  4803  eqsn  4833  pr1eqbg  4858  disjprgw  5144  disjprg  5145  disjxun  5147  opthwiener  5515  opthprc  5741  frxp2  8130  swoord1  8734  brwdomn0  9564  fpwwe2lem12  10637  ne0gt0  11319  xrinfmss  13289  sumsplit  15714  sadadd2lem2  16391  coprm  16648  vdwlem11  16924  lvecvscan  20724  lvecvscan2  20725  mplcoe1  21592  mplcoe5  21595  maducoeval2  22142  xrsxmet  24325  itg2split  25267  plydiveu  25811  quotcan  25822  coseq1  26034  angrtmuld  26313  leibpilem2  26446  leibpi  26447  wilthlem2  26573  tgldimor  27753  tgcolg  27805  axcontlem7  28228  elntg2  28243  nb3grprlem2  28638  eupth2lem2  29472  eupth2lem3lem6  29486  nmlnogt0  30050  hvmulcan  30325  hvmulcan2  30326  rmounid  31735  disjunsn  31825  xrdifh  31991  bj-biorfi  35461  bj-snmoore  35994  nlpineqsn  36289  wl-ifp-ncond1  36345  itgaddnclem2  36547  biorfd  37097  elpadd0  38680  fsuppind  41162  or3or  42774