Theorem biorf 695

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 103   ∨ wo 661

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 577  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biortn  696  pm5.61  740  pm5.55dc  852  euor  1967  eueq3dc  2766  difprsnss  3524  opthprc  4409  frecsuclem3  6013  swoord1  6158  indpi  6532  enq0tr  6624  mulap0r  7715  mulge0  7719  leltap  7724  ap0gt0  7738  coprm  10523