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  4341  opthprc  4828  frecabcl  6674  frecsuclem  6681  swoord1  6840  indpi  7715  enq0tr  7807  mulap0r  8951  mulge0  8955  leltap  8961  ap0gt0  8976  sumsplitdc  12224  coprm  12948  gzsumval2  13773  bdbl  15729  eupth2lem1  16904  eupth2lem2dc  16905  eupth2lem3lem6fi  16917  subctctexmid  17235