Theorem biorf 950

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  biortn  951  biorfi  952  pm5.55  963  pm5.75  1046  3bior1fd  1506  3bior2fd  1508  norasslem3  1566  euor  2637  euorv  2638  euor2  2639  eueq3  3669  unineq  4234  ifor  4537  difprsnss  4762  eqsn  4790  pr1eqbg  4817  disjprg  5099  disjxun  5101  opthwiener  5487  swoord1  8743  brwdomn0  9556  fpwwe2lem12  10720  ne0gt0  11408  xrinfmss  13433  sumsplit  15927  sadadd2lem2  16613  coprm  16880  vdwlem11  17162  lvecvscan  21382  lvecvscan2  21383  mplcoe1  22339  mplcoe5  22342  maducoeval2  22948  xrsxmet  25122  itg2split  26063  plydiveu  26612  quotcan  26625  coseq1  26846  angrtmuld  27129  leibpilem2  27262  leibpi  27263  wilthlem2  27389  tgldimor  28958  tgcolg  29010  dfprlng2  29418  axcontlem7  29541  elntg2  29556  nb3grprlem2  29955  eupth2lem2  30813  eupth2lem3lem6  30827  nmlnogt0  31392  hvmulcan  31667  hvmulcan2  31668  rmounid  33084  disjunsn  33181  xrdifh  33365  bj-snmoore  38014  nlpineqsn  38311  wl-ifp-ncond1  38367  itgaddnclem2  38577  biorfd  39149  elpadd0  40846  fsuppind  43598  frlmnzcoordsca  43638  or3or  45008