Theorem biorf 746

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

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

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 616  ax-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  747  pm5.61  796  pm5.55dc  915  3bior1fd  1364  3bior2fd  1366  euor  2081  eueq3dc  2951  ifordc  3615  difprsnss  3776  exmidsssn  4253  opthprc  4733  frecabcl  6497  frecsuclem  6504  swoord1  6661  indpi  7470  enq0tr  7562  mulap0r  8703  mulge0  8707  leltap  8713  ap0gt0  8728  sumsplitdc  11813  coprm  12536  gsumval2  13299  bdbl  15045  subctctexmid  16072