Theorem biorf 744

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 708

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 615  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  745  pm5.61  794  pm5.55dc  913  euor  2052  eueq3dc  2913  ifordc  3575  difprsnss  3732  exmidsssn  4204  opthprc  4679  frecabcl  6402  frecsuclem  6409  swoord1  6566  indpi  7343  enq0tr  7435  mulap0r  8574  mulge0  8578  leltap  8584  ap0gt0  8599  sumsplitdc  11442  coprm  12146  bdbl  14088  subctctexmid  14835