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  2611  euorv  2612  euor2  2613  eueq3  3657  unineq  4228  ifor  4521  difprsnss  4744  eqsn  4772  pr1eqbg  4800  disjprg  5081  disjxun  5083  opthwiener  5468  swoord1  8676  brwdomn0  9484  fpwwe2lem12  10565  ne0gt0  11251  xrinfmss  13262  sumsplit  15730  sadadd2lem2  16419  coprm  16681  vdwlem11  16962  lvecvscan  21109  lvecvscan2  21110  mplcoe1  22015  mplcoe5  22018  maducoeval2  22605  xrsxmet  24775  itg2split  25716  plydiveu  26264  quotcan  26275  coseq1  26489  angrtmuld  26772  leibpilem2  26905  leibpi  26906  wilthlem2  27032  tgldimor  28570  tgcolg  28622  axcontlem7  29039  elntg2  29054  nb3grprlem2  29450  eupth2lem2  30289  eupth2lem3lem6  30303  nmlnogt0  30868  hvmulcan  31143  hvmulcan2  31144  rmounid  32564  disjunsn  32664  xrdifh  32853  bj-snmoore  37425  nlpineqsn  37724  wl-ifp-ncond1  37780  itgaddnclem2  38000  biorfd  38558  elpadd0  40255  fsuppind  43023  or3or  44450