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  2064  eueq3dc  2926  ifordc  3588  difprsnss  3745  exmidsssn  4220  opthprc  4695  frecabcl  6424  frecsuclem  6431  swoord1  6588  indpi  7371  enq0tr  7463  mulap0r  8602  mulge0  8606  leltap  8612  ap0gt0  8627  sumsplitdc  11472  coprm  12176  bdbl  14460  subctctexmid  15209