Theorem biorf 752

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

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

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 620  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  753  pm5.61  802  pm5.55dc  921  3bior1fd  1389  3bior2fd  1391  euor  2106  eueq3dc  2991  ifordc  3664  difprsnss  3832  exmidsssn  4315  opthprc  4801  frecabcl  6630  frecsuclem  6637  swoord1  6796  indpi  7657  enq0tr  7749  mulap0r  8889  mulge0  8893  leltap  8899  ap0gt0  8914  sumsplitdc  12118  coprm  12841  gsumval2  13610  bdbl  15368  eupth2lem1  16453  eupth2lem2dc  16454  eupth2lem3lem6fi  16466  subctctexmid  16774