Theorem biorf 950

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  biortn  951  biorfi  952  pm5.55  963  pm5.75  1046  3bior1fd  1507  3bior2fd  1509  norasslem3  1566  euor  2639  euorv  2640  euor2  2641  eueq3  3672  unineq  4236  ifor  4540  difprsnss  4764  eqsn  4790  pr1eqbg  4817  disjprg  5104  disjxun  5106  opthwiener  5494  swoord1  8788  brwdomn0  9600  fpwwe2lem12  10766  ne0gt0  11454  xrinfmss  13480  sumsplit  15978  sadadd2lem2  16664  coprm  16931  vdwlem11  17213  lvecvscan  21440  lvecvscan2  21441  mplcoe1  22401  mplcoe5  22404  maducoeval2  23010  xrsxmet  25184  itg2split  26125  plydiveu  26674  quotcan  26687  coseq1  26910  angrtmuld  27193  leibpilem2  27326  leibpi  27327  wilthlem2  27453  tgldimor  29022  tgcolg  29074  dfprlng2  29482  axcontlem7  29605  elntg2  29620  nb3grprlem2  30019  eupth2lem2  30877  eupth2lem3lem6  30891  nmlnogt0  31456  hvmulcan  31731  hvmulcan2  31732  rmounid  33190  disjunsn  33286  xrdifh  33468  bj-snmoore  38304  nlpineqsn  38599  wl-ifp-ncond1  38655  itgaddnclem2  38865  biorfd  39435  elpadd0  41132  fsuppind  43884  frlmnzcoordsca  43924  or3or  45284