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  1565  euor  2636  euorv  2637  euor2  2638  eueq3  3668  unineq  4233  ifor  4536  difprsnss  4758  eqsn  4784  pr1eqbg  4811  disjprg  5098  disjxun  5100  opthwiener  5486  swoord1  8754  brwdomn0  9567  fpwwe2lem12  10731  ne0gt0  11419  xrinfmss  13444  sumsplit  15940  sadadd2lem2  16626  coprm  16893  vdwlem11  17175  lvecvscan  21395  lvecvscan2  21396  mplcoe1  22352  mplcoe5  22355  maducoeval2  22961  xrsxmet  25135  itg2split  26076  plydiveu  26625  quotcan  26638  coseq1  26859  angrtmuld  27142  leibpilem2  27275  leibpi  27276  wilthlem2  27402  tgldimor  28971  tgcolg  29023  dfprlng2  29431  axcontlem7  29554  elntg2  29569  nb3grprlem2  29968  eupth2lem2  30826  eupth2lem3lem6  30840  nmlnogt0  31405  hvmulcan  31680  hvmulcan2  31681  rmounid  33139  disjunsn  33236  xrdifh  33419  bj-snmoore  38127  nlpineqsn  38425  wl-ifp-ncond1  38481  itgaddnclem2  38691  biorfd  39263  elpadd0  40960  fsuppind  43712  frlmnzcoordsca  43752  or3or  45117