Theorem biorf 949

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

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

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 861

This theorem is referenced by:  biortn  950  biorfi  951  pm5.55  963  pm5.75  1046  3bior1fd  1506  3bior2fd  1508  norasslem3  1566  euor  2639  euorv  2640  euor2  2641  eueq3  3674  unineq  4241  ifor  4542  difprsnss  4767  eqsn  4795  pr1eqbg  4822  disjprg  5105  disjxun  5107  opthwiener  5497  swoord1  8723  brwdomn0  9527  fpwwe2lem12  10622  ne0gt0  11310  xrinfmss  13331  sumsplit  15815  sadadd2lem2  16503  coprm  16765  vdwlem11  17046  lvecvscan  21235  lvecvscan2  21236  mplcoe1  22188  mplcoe5  22191  maducoeval2  22797  xrsxmet  24967  itg2split  25908  plydiveu  26459  quotcan  26470  coseq1  26690  angrtmuld  26973  leibpilem2  27106  leibpi  27107  wilthlem2  27233  tgldimor  28771  tgcolg  28823  dfprlng2  29197  axcontlem7  29320  elntg2  29335  nb3grprlem2  29731  eupth2lem2  30570  eupth2lem3lem6  30584  nmlnogt0  31149  hvmulcan  31424  hvmulcan2  31425  rmounid  32841  disjunsn  32939  xrdifh  33125  bj-snmoore  37755  nlpineqsn  38054  wl-ifp-ncond1  38110  itgaddnclem2  38330  biorfd  38886  elpadd0  40583  fsuppind  43322  or3or  44749