Theorem biorf 734

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

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

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 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biortn  735  pm5.61  784  pm5.55dc  899  euor  2032  eueq3dc  2886  difprsnss  3694  exmidsssn  4162  opthprc  4634  frecabcl  6340  frecsuclem  6347  swoord1  6502  indpi  7245  enq0tr  7337  mulap0r  8473  mulge0  8477  leltap  8483  ap0gt0  8498  sumsplitdc  11311  coprm  11998  bdbl  12863  subctctexmid  13533