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  2108  eueq3dc  2994  ifordc  3668  difprsnss  3837  exmidsssn  4320  opthprc  4806  frecabcl  6643  frecsuclem  6650  swoord1  6809  indpi  7673  enq0tr  7765  mulap0r  8906  mulge0  8910  leltap  8916  ap0gt0  8931  sumsplitdc  12143  coprm  12866  gsumval2  13660  bdbl  15494  eupth2lem1  16579  eupth2lem2dc  16580  eupth2lem3lem6fi  16592  subctctexmid  16900