Theorem biorf 739

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

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

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 610  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biortn  740  pm5.61  789  pm5.55dc  908  euor  2045  eueq3dc  2904  ifordc  3564  difprsnss  3718  exmidsssn  4188  opthprc  4662  frecabcl  6378  frecsuclem  6385  swoord1  6542  indpi  7304  enq0tr  7396  mulap0r  8534  mulge0  8538  leltap  8544  ap0gt0  8559  sumsplitdc  11395  coprm  12098  bdbl  13297  subctctexmid  14034