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  2636  euorv  2637  euor2  2638  eueq3  3669  unineq  4234  ifor  4537  difprsnss  4762  eqsn  4790  pr1eqbg  4817  disjprg  5099  disjxun  5101  opthwiener  5491  swoord1  8729  brwdomn0  9541  fpwwe2lem12  10651  ne0gt0  11339  xrinfmss  13362  sumsplit  15854  sadadd2lem2  16540  coprm  16802  vdwlem11  17083  lvecvscan  21298  lvecvscan2  21299  mplcoe1  22253  mplcoe5  22256  maducoeval2  22862  xrsxmet  25036  itg2split  25977  plydiveu  26528  quotcan  26541  coseq1  26762  angrtmuld  27045  leibpilem2  27178  leibpi  27179  wilthlem2  27305  tgldimor  28844  tgcolg  28896  dfprlng2  29304  axcontlem7  29427  elntg2  29442  nb3grprlem2  29841  eupth2lem2  30699  eupth2lem3lem6  30713  nmlnogt0  31278  hvmulcan  31553  hvmulcan2  31554  rmounid  32970  disjunsn  33067  xrdifh  33251  bj-snmoore  37863  nlpineqsn  38162  wl-ifp-ncond1  38218  itgaddnclem2  38428  biorfd  38985  elpadd0  40682  fsuppind  43436  or3or  44863