Theorem biorf 419

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  biortn  420  pm5.61  745  pm5.55  937  pm5.75  974  3bior1fd  1430  3bior2fd  1432  euor  2500  euor2  2502  eueq3  3348  unineq  3836  ifor  4085  difprsnss  4270  eqsn  4301  disjprg  4578  disjxun  4581  opthwiener  4901  opthprc  5089  swoord1  7660  brwdomn0  8357  fpwwe2lem13  9343  ne0gt0  10021  xrinfmss  12012  sumsplit  14341  sadadd2lem2  15010  coprm  15261  vdwlem11  15533  lvecvscan  18932  lvecvscan2  18933  mplcoe1  19286  mplcoe5  19289  maducoeval2  20265  xrsxmet  22420  itg2split  23322  plydiveu  23857  quotcan  23868  coseq1  24078  angrtmuld  24338  leibpilem2  24468  leibpi  24469  wilthlem2  24595  tgldimor  25197  tgcolg  25249  axcontlem7  25650  nb3graprlem2  25981  eupath2lem2  26505  eupath2lem3  26506  nmlnogt0  27036  hvmulcan  27313  hvmulcan2  27314  disjunsn  28789  xrdifh  28932  bj-biorfi  31741  itgaddnclem2  32639  elpadd0  34113  or3or  37339  pr1eqbg  40313  nb3grprlem2  40609  eupth2lem2  41387  eupth2lem3lem6  41401