Theorem biorf 733

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104   ∨ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 604  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biortn  734  pm5.61  783  pm5.55dc  898  euor  2025  eueq3dc  2858  difprsnss  3658  exmidsssn  4125  opthprc  4590  frecabcl  6296  frecsuclem  6303  swoord1  6458  indpi  7150  enq0tr  7242  mulap0r  8377  mulge0  8381  leltap  8387  ap0gt0  8402  sumsplitdc  11201  coprm  11822  bdbl  12672  subctctexmid  13196