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  2026  eueq3dc  2862  difprsnss  3666  exmidsssn  4133  opthprc  4598  frecabcl  6304  frecsuclem  6311  swoord1  6466  indpi  7174  enq0tr  7266  mulap0r  8401  mulge0  8405  leltap  8411  ap0gt0  8426  sumsplitdc  11233  coprm  11858  bdbl  12711  subctctexmid  13369