Theorem biorf 749

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

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

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 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biortn  750  pm5.61  799  pm5.55dc  918  3bior1fd  1386  3bior2fd  1388  euor  2103  eueq3dc  2977  ifordc  3644  difprsnss  3806  exmidsssn  4286  opthprc  4770  frecabcl  6551  frecsuclem  6558  swoord1  6717  indpi  7540  enq0tr  7632  mulap0r  8773  mulge0  8777  leltap  8783  ap0gt0  8798  sumsplitdc  11958  coprm  12681  gsumval2  13445  bdbl  15192  subctctexmid  16425