Theorem biorf 756

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  biortn  757  pm5.61  806  pm5.55dc  925  3bior1fd  1393  3bior2fd  1395  euor  2112  eueq3dc  3000  ifordc  3682  difprsnss  3853  exmidsssn  4339  opthprc  4826  frecabcl  6670  frecsuclem  6677  swoord1  6836  indpi  7710  enq0tr  7802  mulap0r  8946  mulge0  8950  leltap  8956  ap0gt0  8971  sumsplitdc  12218  coprm  12942  gzsumval2  13767  bdbl  15695  eupth2lem1  16865  eupth2lem2dc  16866  eupth2lem3lem6fi  16878  subctctexmid  17196