Theorem biorf 937

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 848

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 207  df-or 849

This theorem is referenced by:  biortn  938  biorfi  939  pm5.55  951  pm5.75  1031  3bior1fd  1477  3bior2fd  1479  norasslem3  1536  euor  2611  euorv  2612  euor2  2613  eueq3  3717  unineq  4288  ifor  4580  difprsnss  4799  eqsn  4829  pr1eqbg  4857  disjprg  5139  disjxun  5141  opthwiener  5519  swoord1  8777  brwdomn0  9609  fpwwe2lem12  10682  ne0gt0  11366  xrinfmss  13352  sumsplit  15804  sadadd2lem2  16487  coprm  16748  vdwlem11  17029  lvecvscan  21113  lvecvscan2  21114  mplcoe1  22055  mplcoe5  22058  maducoeval2  22646  xrsxmet  24831  itg2split  25784  plydiveu  26340  quotcan  26351  coseq1  26567  angrtmuld  26851  leibpilem2  26984  leibpi  26985  wilthlem2  27112  tgldimor  28510  tgcolg  28562  axcontlem7  28985  elntg2  29000  nb3grprlem2  29398  eupth2lem2  30238  eupth2lem3lem6  30252  nmlnogt0  30816  hvmulcan  31091  hvmulcan2  31092  rmounid  32514  disjunsn  32607  xrdifh  32782  bj-snmoore  37114  nlpineqsn  37409  wl-ifp-ncond1  37465  itgaddnclem2  37686  biorfd  38232  elpadd0  39811  fsuppind  42600  or3or  44036