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  7709  enq0tr  7801  mulap0r  8945  mulge0  8949  leltap  8955  ap0gt0  8970  sumsplitdc  12215  coprm  12939  gzsumval2  13763  bdbl  15653  eupth2lem1  16797  eupth2lem2dc  16798  eupth2lem3lem6fi  16810  subctctexmid  17128