Theorem biorf 734

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104   ∨ wo 698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biortn  735  pm5.61  784  pm5.55dc  903  euor  2040  eueq3dc  2900  difprsnss  3711  exmidsssn  4181  opthprc  4655  frecabcl  6367  frecsuclem  6374  swoord1  6530  indpi  7283  enq0tr  7375  mulap0r  8513  mulge0  8517  leltap  8523  ap0gt0  8538  sumsplitdc  11373  coprm  12076  bdbl  13143  subctctexmid  13881