Theorem biorf 933

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  biortn  934  pm5.55  945  pm5.75  1025  3bior1fd  1471  3bior2fd  1473  norasslem3  1532  euor  2695  euorv  2696  euor2  2697  eueq3  3702  unineq  4254  ifor  4519  difprsnss  4732  eqsn  4762  pr1eqbg  4787  disjprgw  5061  disjprg  5062  disjxun  5064  opthwiener  5404  opthprc  5616  swoord1  8320  brwdomn0  9033  fpwwe2lem13  10064  ne0gt0  10745  xrinfmss  12704  sumsplit  15123  sadadd2lem2  15799  coprm  16055  vdwlem11  16327  lvecvscan  19883  lvecvscan2  19884  mplcoe1  20246  mplcoe5  20249  maducoeval2  21249  xrsxmet  23417  itg2split  24350  plydiveu  24887  quotcan  24898  coseq1  25110  angrtmuld  25386  leibpilem2  25519  leibpi  25520  wilthlem2  25646  tgldimor  26288  tgcolg  26340  axcontlem7  26756  elntg2  26771  nb3grprlem2  27163  eupth2lem2  27998  eupth2lem3lem6  28012  nmlnogt0  28574  hvmulcan  28849  hvmulcan2  28850  rmounid  30259  disjunsn  30344  xrdifh  30503  bj-biorfi  33917  bj-snmoore  34408  nlpineqsn  34692  itgaddnclem2  34966  elpadd0  36960  or3or  40420