Theorem biorf 698

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 103   ∨ wo 664

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 580  ax-io 665

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biortn  699  pm5.61  743  pm5.55dc  857  euor  1974  eueq3dc  2787  difprsnss  3570  opthprc  4477  frecabcl  6146  frecsuclem  6153  swoord1  6301  indpi  6880  enq0tr  6972  mulap0r  8068  mulge0  8072  leltap  8077  ap0gt0  8091  sumsplitdc  10789  coprm  11216