Theorem biorf 752

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 620  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  753  pm5.61  802  pm5.55dc  921  3bior1fd  1389  3bior2fd  1391  euor  2105  eueq3dc  2981  ifordc  3651  difprsnss  3816  exmidsssn  4298  opthprc  4783  frecabcl  6608  frecsuclem  6615  swoord1  6774  indpi  7605  enq0tr  7697  mulap0r  8837  mulge0  8841  leltap  8847  ap0gt0  8862  sumsplitdc  12056  coprm  12779  gsumval2  13543  bdbl  15297  eupth2lem1  16382  eupth2lem2dc  16383  eupth2lem3lem6fi  16395  subctctexmid  16705