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  3658  unineq  4229  ifor  4522  difprsnss  4743  eqsn  4773  pr1eqbg  4801  disjprg  5082  disjxun  5084  opthwiener  5462  swoord1  8669  brwdomn0  9477  fpwwe2lem12  10556  ne0gt0  11242  xrinfmss  13253  sumsplit  15721  sadadd2lem2  16410  coprm  16672  vdwlem11  16953  lvecvscan  21101  lvecvscan2  21102  mplcoe1  22025  mplcoe5  22028  maducoeval2  22615  xrsxmet  24785  itg2split  25726  plydiveu  26275  quotcan  26286  coseq1  26502  angrtmuld  26785  leibpilem2  26918  leibpi  26919  wilthlem2  27046  tgldimor  28584  tgcolg  28636  axcontlem7  29053  elntg2  29068  nb3grprlem2  29464  eupth2lem2  30304  eupth2lem3lem6  30318  nmlnogt0  30883  hvmulcan  31158  hvmulcan2  31159  rmounid  32579  disjunsn  32679  xrdifh  32868  bj-snmoore  37441  nlpineqsn  37738  wl-ifp-ncond1  37794  itgaddnclem2  38014  biorfd  38572  elpadd0  40269  fsuppind  43037  or3or  44468