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  1478  3bior2fd  1480  norasslem3  1538  euor  2612  euorv  2613  euor2  2614  eueq3  3671  unineq  4242  ifor  4536  difprsnss  4757  eqsn  4787  pr1eqbg  4815  disjprg  5096  disjxun  5098  opthwiener  5470  swoord1  8678  brwdomn0  9486  fpwwe2lem12  10565  ne0gt0  11250  xrinfmss  13237  sumsplit  15703  sadadd2lem2  16389  coprm  16650  vdwlem11  16931  lvecvscan  21078  lvecvscan2  21079  mplcoe1  22004  mplcoe5  22007  maducoeval2  22596  xrsxmet  24766  itg2split  25718  plydiveu  26274  quotcan  26285  coseq1  26502  angrtmuld  26786  leibpilem2  26919  leibpi  26920  wilthlem2  27047  tgldimor  28586  tgcolg  28638  axcontlem7  29055  elntg2  29070  nb3grprlem2  29466  eupth2lem2  30306  eupth2lem3lem6  30320  nmlnogt0  30884  hvmulcan  31159  hvmulcan2  31160  rmounid  32580  disjunsn  32680  xrdifh  32870  bj-snmoore  37363  nlpineqsn  37660  wl-ifp-ncond1  37716  itgaddnclem2  37927  biorfd  38485  elpadd0  40182  fsuppind  42945  or3or  44376