Theorem biorf 935

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 887	. 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  936  pm5.55  947  pm5.75  1027  3bior1fd  1475  3bior2fd  1477  norasslem3  1537  euor  2606  euorv  2607  euor2  2608  eueq3  3672  unineq  4242  ifor  4545  difprsnss  4764  eqsn  4794  pr1eqbg  4819  disjprgw  5105  disjprg  5106  disjxun  5108  opthwiener  5476  opthprc  5701  frxp2  8081  swoord1  8686  brwdomn0  9514  fpwwe2lem12  10587  ne0gt0  11269  xrinfmss  13239  sumsplit  15664  sadadd2lem2  16341  coprm  16598  vdwlem11  16874  lvecvscan  20631  lvecvscan2  20632  mplcoe1  21475  mplcoe5  21478  maducoeval2  22026  xrsxmet  24209  itg2split  25151  plydiveu  25695  quotcan  25706  coseq1  25918  angrtmuld  26195  leibpilem2  26328  leibpi  26329  wilthlem2  26455  tgldimor  27507  tgcolg  27559  axcontlem7  27982  elntg2  27997  nb3grprlem2  28392  eupth2lem2  29226  eupth2lem3lem6  29240  nmlnogt0  29802  hvmulcan  30077  hvmulcan2  30078  rmounid  31487  disjunsn  31579  xrdifh  31751  bj-biorfi  35124  bj-snmoore  35657  nlpineqsn  35952  wl-ifp-ncond1  36008  itgaddnclem2  36210  biorfd  36761  elpadd0  38345  fsuppind  40823  or3or  42417