Theorem biorf 745

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  746  pm5.61  795  pm5.55dc  914  euor  2071  eueq3dc  2938  ifordc  3601  difprsnss  3761  exmidsssn  4236  opthprc  4715  frecabcl  6466  frecsuclem  6473  swoord1  6630  indpi  7426  enq0tr  7518  mulap0r  8659  mulge0  8663  leltap  8669  ap0gt0  8684  sumsplitdc  11614  coprm  12337  gsumval2  13099  bdbl  14823  subctctexmid  15731