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  3805  exmidsssn  4285  opthprc  4769  frecabcl  6543  frecsuclem  6550  swoord1  6707  indpi  7525  enq0tr  7617  mulap0r  8758  mulge0  8762  leltap  8768  ap0gt0  8783  sumsplitdc  11938  coprm  12661  gsumval2  13425  bdbl  15171  subctctexmid  16325